no goals
ι : Type u_2
κ : Type ?u.64
R : Type ?u.67
α : Type u_1
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂✝ a₂ : α
h : HasSum f a₁
⊢ HasSum (fun i => a₂ * f i) (a₂ * a₁)
simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)