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