no goals
α : Type u_1
β : Type u_2
γ : Type ?u.14510
δ : Type ?u.14513
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
⊢ HasSum (fun x => 0) 0
simp [HasSum, tendsto_const_nhds]