English
Let r be an element of a monoid R and f a finitely supported function ι →₀ M, with M an additive monoid and R acting on M. Then toFinsupp respects scalar multiplication: toFinsupp(r • f) = r • toFinsupp(f).
Русский
Пусть r ∈ R и f ∈ (ι →₀ M), где M — аддитивная монада и R действует на M. Тогда toFinsupp сохраняет скалярное умножение: toFinsupp(r • f) = r • toFinsupp(f).
LaTeX
$$$\\bigl(toFinsupp (r \\cdot f) : ι \\to_0 M\\bigr) = r \\cdot toFinsupp f$$$
Lean4
@[simp]
theorem toFinsupp_smul [Monoid R] [AddMonoid M] [DistribMulAction R M] [∀ m : M, Decidable (m ≠ 0)] (r : R)
(f : Π₀ _ : ι, M) : (toFinsupp (r • f) : ι →₀ M) = r • toFinsupp f :=
DFunLike.coe_injective <| DFinsupp.coe_smul _ _
