Theorems · Theorem · general algebraic systems

Finsupp.sum_update_add

∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : AddZeroClass α] [inst_1 : AddCommMonoid β] (f : ι →₀ α) (i : ι)
  (a : α) (g : ι → α → β),
  (∀ (i : ι), g i 0 = 0) →
    (∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂) → (f.update i a).sum g + g i (f i) = f.sum g + g i a

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddCommMonoid