LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.InfiniteSum.Basic

theorem DiscreteTopology.summable_iff_eventually_zero {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [DiscreteTopology E] {ι : Type u_2} (f : ι → E) : Summable f ↔ ∀ᶠ (n : ι) in Filter.cofinite, f n = 0