English
In a module over a ring, the scalar c acting on the finsum equals the finsum of the scalars: c • ∑ᶠ f i = ∑ᶠ (c • f i) when the support is finite.
Русский
В модуле над кольцом скалярное умножение на c распространяется на finsum: c•∑ f(i) = ∑ c•f(i) при конечной опоре.
LaTeX
$$$\\displaystyle c \\cdot \\sum\\ᶠ i, f i = \\sum\\ᶠ i, c \\cdot f i$ (при конечной опоре)$$
Lean4
/-- See also `finsum_smul` for a version that works even when the support of `f` is not finite,
but with slightly stronger typeclass requirements. -/
theorem finsum_smul' {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] {f : ι → R} (hf : (support f).Finite)
(x : M) : (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x :=
((smulAddHom R M).flip x).map_finsum hf
