Theorems · Theorem · general algebraic systems

DFinsupp.mapRange_single

∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β₁ i)]
  [inst_2 : (i : ι) → Zero (β₂ i)] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {i : ι} {b : β₁ i},
  (DFinsupp.mapRange f hf fun₀ | i => b) = fun₀ | i => f i b

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

8 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqZeroZero