Theorems · Theorem · general algebraic systems

DFinsupp.mapRange_def

∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β₁ i)]
  [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)] {f : (i : ι) → β₁ i → β₂ i}
  {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i},
  DFinsupp.mapRange f hf g = DFinsupp.mk g.support fun i => f (↑i) (g ↑i)

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

3 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqZeroZeroDecidable