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