English
In a module M over a ring R with NoZeroSMulDivisors, for any c ∈ R and f : ι → M, we have c • ∑ᶠ i, f(i) = ∑ᶠ i, c • f(i).
Русский
В модуле M над кольцом R с NoZeroSMulDivisors для любого элемента c ∈ R и функции f: ι → M выполняется c · ∑ᶠ i, f(i) = ∑ᶠ i, c · f(i).
LaTeX
$$$$ c\cdot\left(\sum^{\mathrm{fin}}_{i} f(i)\right) = \sum^{\mathrm{fin}}_{i} (c\cdot f(i)). $$$$
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 `smul_finsum'`. -/
theorem smul_finsum {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (c : R)
(f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i :=
by
rcases eq_or_ne c 0 with (rfl | hc)
· simp
· exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
