toFinsupp_add — Mathlib

English

In the DFinsupp setting, addition is preserved by toFinsupp: toFinsupp (f + g) = toFinsupp f + toFinsupp g.

Русский

В DFinsupp сохранение сложения: toFinsupp (f + g) = toFinsupp f + toFinsupp g.

LaTeX

$$(toFinsupp (f + g) : ι →₀ M) = toFinsupp f + toFinsupp g$$

Lean4

@[simp]
theorem toFinsupp_add [AddZeroClass M] [∀ m : M, Decidable (m ≠ 0)] (f g : Π₀ _ : ι, M) :
    (toFinsupp (f + g) : ι →₀ M) = toFinsupp f + toFinsupp g :=
  DFunLike.coe_injective <| DFinsupp.coe_add _ _

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