no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19688
δ : Type ?u.19691
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
h : ¬Summable f
⊢ (∑' (b : β), f b) = 0
simp [tsum_def, h]