English
In a module M over a ring R with NoZeroSMulDivisors, for any f : ι → R and x ∈ M, the infinited sum distributes over scalar action:
(∑ᶠ i, f(i)) • x = ∑ᶠ i, f(i) • x.
Русский
В модуле M над кольцом R с свойством NoZeroSMulDivisors бесконечная сумма распределяется над действием скаляра:
(∑ᶠ i, f(i)) · x = ∑ᶠ i, f(i) · x.
LaTeX
$$$$ \biggl(\sum^{\mathrm{fin}}_{i} f(i)\biggr) \cdot x = \sum^{\mathrm{fin}}_{i} (f(i) \cdot x). $$$$
Lean4
/-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is
infinite. For a more usual version assuming `(support f).Finite` instead, see `finsum_smul'`. -/
theorem finsum_smul {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : ι → R) (x : M) :
(∑ᶠ i, f i) • x = ∑ᶠ i, f i • x := by
rcases eq_or_ne x 0 with (rfl | hx)
· simp
· exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _
