English
In a module, the finsum distributes over scalar multiplication on the left: (c) • ∑ᶠ i, f i = ∑ᶠ i, c • f i.
Русский
В модуле сумма распределяется слева по скалярному умножению: c•∑ f(i) = ∑ c•f(i).
LaTeX
$$$\\displaystyle c \\cdot \\sum\\ᶠ i, f i = \\sum\\ᶠ i, c \\cdot f i$$$
Lean4
/-- See also `smul_finsum` for a version that works even when the support of `f` is not finite,
but with slightly stronger typeclass requirements. -/
theorem smul_finsum' {R M : Type*} [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (c : R) {f : ι → M}
(hf : (support f).Finite) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i :=
(DistribMulAction.toAddMonoidHom M c).map_finsum hf
