English
If the ambient semiring R has no zero divisors, then multiplication commutes with finsums: for any f: α → R and r ∈ R, (r * ∑ᶠ a, f a) = ∑ᶠ a, r * f a. The finiteness of the support is not assumed here since r multiplies the entire finsum.
Русский
Если в кольце без нулевых делителей выполняются распределительные законы, тогда умножение на r слева и справа проходит через finsum: для любой f: α → R и r ∈ R имеем (r · ∑ᶠ a, f a) = ∑ᶠ a, r · f a.
LaTeX
$$$ (NoZeroDivisors\\, R) \\\\Rightarrow (r \\cdot \\\\sum^\\\\mathrm{f}_{a \\in \\alpha} f(a)) = \\\\sum^\\\\mathrm{f}_{a \\in \\alpha} (r \\cdot f(a)) $$$
Lean4
/-- If `R` has no zero divisors, then multiplication commutes with finsums. See `mul_finsum'` for a
statement assuming finiteness of support.
-/
theorem mul_finsum {R : Type*} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] (f : α → R) (r : R) :
(r * ∑ᶠ a : α, f a) = ∑ᶠ a : α, r * f a := by
by_cases hr : r = 0
· simp_all
by_cases h : f.support.Finite
· exact mul_finsum' f r h
simp [finsum_def, h, (by aesop : (r * f ·).support = f.support)]
