no goals
ι : Type u_2
κ : Type ?u.53822
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : Summable f
⊢ (∑' (i : ι), f i) = 0 ↔ ∀ (x : ι), f x = 0
rw [← hasSum_zero_iff, hf.hasSum_iff]