English
If R has no zero divisors, then multiplication commutes with finsum over a finite index set: (∑ᶠ a ∈ s, f a) · r = ∑ᶠ a ∈ s, f a · r.
Русский
Если в кольце без нулевых делителей, то умножение через finsum по подмножеству сохраняется: (∑ᶠ a ∈ s, f a) · r = ∑ᶠ a ∈ s, f a · r.
LaTeX
$$$ (NoZeroDivisors\\, R) \\\\Rightarrow (\\\\sum^\\\\mathrm{f}_{a \\in s} f(a)) \\\\cdot r = \\\\sum^\\\\mathrm{f}_{a \\in s} (f(a) \\\\cdot r) $$$
Lean4
/-- If `R` has no zero divisors, then multiplication commutes with `finsum_mem`. See `finsum_mem_mul'`
for a statement assuming finiteness of support.
-/
theorem finsum_mem_mul {R : Type*} [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {s : Set α} (f : α → R) (r : R) :
(∑ᶠ a ∈ s, f a) * r = ∑ᶠ a ∈ s, f a * r := by
rw [finsum_mul]
congr
ext a
by_cases h : a ∈ s <;> simp_all
