English
Let s be a finite set. For any function f: α → R and any r ∈ R, the finsum over s commutes with left/right multiplication: (∑ᶠ a ∈ s, f a) · r = ∑ᶠ a ∈ s, f a · r.
Русский
Пусть s — конечное множество. Для любой функции f: α → R и любого r ∈ R сумма finsum по s коммутирует с умножением слева/справа: (∑ᶠ a ∈ s, f(a)) · r = ∑ᶠ a ∈ s, f(a) · r.
LaTeX
$$$ (s.Finite) \\\\Rightarrow \\\\left(\\\\sum^\\\\mathrm{f}_{a \\in s} f(a)\\\\right) \\\\cdot r = \\\\sum^\\\\mathrm{f}_{a \\in s} f(a) \\\\cdot r $$$
Lean4
/-- For finite sets, multiplication commutes with `finsum_mem`. See `finsum_mem_mul'` for a statement
assuming finiteness of support.
-/
theorem finsum_mem_mul' {R : Type*} [NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R) (hs : s.Finite) :
(∑ᶠ a ∈ s, f a) * r = ∑ᶠ a ∈ s, f a * r :=
(AddMonoidHom.mulRight r).map_finsum_mem f hs
