Theorems · Theorem · group theory

smul_finsum

∀ {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] (c : R) (f : ι → M), c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i

The torsion-free assumption makes sure that the result holds even when the support of f is infinite. For a more usual version assuming HasFiniteSupport f instead, see smul_finsum'.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringIsDomainAddCommGroupModuleModule.IsTorsionFree