English
Let f and g be finitely supported functions f, g : ι → M with M an additive group. Then applying the toFinsupp map to their difference equals the difference of their images: toFinsupp(f − g) = toFinsupp(f) − toFinsupp(g).
Русский
Пусть f и g — склоняемые к нулю функции f, g: ι → M, где M — аддитивная группа. Тогда применение преобразования toFinsupp к их разности равно разности изображений: toFinsupp(f − g) = toFinsupp(f) − toFinsupp(g).
LaTeX
$$$\\bigl(toFinsupp (f - g) : \\iota \\to_0 M\\bigr) = toFinsupp f - toFinsupp g$$$
Lean4
@[simp]
theorem toFinsupp_sub [AddGroup M] [∀ m : M, Decidable (m ≠ 0)] (f g : Π₀ _ : ι, M) :
(toFinsupp (f - g) : ι →₀ M) = toFinsupp f - toFinsupp g :=
DFunLike.coe_injective <| DFinsupp.coe_sub _ _
