English
Infinit sums commute with scalar multiplication for group scalars: ∑' i, g • f i = g • ∑' i, f i.
Русский
Бесконечные суммы коммутируют со скалярным умножением в группе: ∑' i, g • f i = g • ∑' i, f i.
LaTeX
$$$$ \sum' i, g \cdot f i = g \cdot \sum' i, f i. $$$$
Lean4
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a `Group`, but
not requiring any summability hypothesis. -/
theorem tsum_const_smul' {γ : Type*} [Group γ] [DistribMulAction γ α] [ContinuousConstSMul γ α] [T2Space α] (g : γ) :
∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i :=
((Homeomorph.smul g).isClosedEmbedding.map_tsum f (g :=
show α ≃+ α from
{ AddMonoidHom.smulLeft g with invFun := AddMonoidHom.smulLeft g⁻¹, left_inv a := by simp,
right_inv a := by simp })).symm
