English
If R has no zero divisors, then finsum commutes with multiplication: (∑ᶠ a, f a) · r = ∑ᶠ a, f a · r.
Русский
Если в кольце без нулевых делителей существует, то finsum коммутирует с умножением: (∑ᶠ a, f a) · r = ∑ᶠ a, f a · r.
LaTeX
$$$ (NoZeroDivisors\\, R) \\\\Rightarrow (\\\\sum^\\\\mathrm{f}_{a} f(a)) \\\\cdot r = \\\\sum^\\\\mathrm{f}_{a} (f(a) \\\\cdot r) $$$
Lean4
/-- If `R` has no zero divisors, then multiplication commutes with finsums. See `finsum_mul'` for a
statement assuming finiteness of support.
-/
theorem finsum_mul {R : Type*} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] (f : α → R) (r : R) :
(∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r := by
by_cases hr : r = 0
· simp_all
by_cases h : f.support.Finite
· exact finsum_mul' f r h
simp [finsum_def, h, (by aesop : (f · * r).support = f.support)]
