no goals
α : Type u_1
β : Type u_2
γ : Type ?u.809017
δ : Type ?u.809020
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
a : α
h : HasSum f a
⊢ HasSum (fun b => Star.star (f b)) (Star.star a)
simpa only using h.map (starAddEquiv : α ≃+ α) continuous_star