sum_single — Mathlib

English

For any DFinsupp f, summing over the single entries yields f itself: f.sum single = f.

Русский

Для произвольного DFinsupp f сумма по единичному отображению даёт само f.

LaTeX

$$$ f.sum\\, \\mathrm{single} = f. $$$

Lean4

@[simp]
theorem sum_single [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i, β i} : f.sum single = f :=
  by
  have := DFunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f
  rw [liftAddHom_apply, sumAddHom_apply] at this
  exact this

Похожие утверждения