English
Infinite sums commute with scalar multiplication in a DivisionSemiring setting.
Русский
Бесконечные суммы коммутируют с умножением на константу в контексте DivisionSemiring.
LaTeX
$$$$ \sum' i, g • f i = g • \sum' i, f i. $$$$
Lean4
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a
`DivisionSemiring`; no summability hypothesis. This could be made to work for a
`[GroupWithZero γ]` if there was such a thing as `DistribMulActionWithZero`. -/
theorem tsum_const_smul'' {γ : Type*} [DivisionSemiring γ] [Module γ α] [ContinuousConstSMul γ α] [T2Space α] (g : γ) :
∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i :=
by
rcases eq_or_ne g 0 with rfl | hg
· simp
· exact tsum_const_smul' (Units.mk0 g hg)
