English
Let R be a (not necessarily unital, not necessarily associative) semiring. If f: α → R has finite support, then for every r ∈ R the right multiplication by r commutes with the finsum: (∑ᶠ a ∈ α, f a) · r = ∑ᶠ a ∈ α, f a · r.
Русский
Пусть R — полуспектр без обязательного единицы и без ассоциативности. Пусть f: α → R имеет конечную опору. Тогда для любого r ∈ R верно, что правое умножение на r переставляет finsum: (∑ᶠ a ∈ α, f(a)) · r = ∑ᶠ a ∈ α, f(a) · r.
LaTeX
$$$ (support\\, f).Finite \\\\Rightarrow \\\\left(\\\\sum^\\\\mathrm{f}_{a \\in \\alpha} f(a)\\\\right) \\\\cdot r = \\\\sum^\\\\mathrm{f}_{a \\in \\alpha} f(a) \\\\cdot r $$$
Lean4
/-- For functions with finite support, multiplication commutes with finsums. See `finsum_mul` for a
statement assuming that `R` has no zero divisors.
-/
theorem finsum_mul' {R : Type*} [NonUnitalNonAssocSemiring R] (f : α → R) (r : R) (h : (support f).Finite) :
(∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
(AddMonoidHom.mulRight r).map_finsum h
