∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasSum f a (SummationFilter.symmetricIcc ℤ) ↔
    Filter.Tendsto (fun N => ∑ n ∈ Finset.Icc (-↑N) ↑N, f n) Filter.atTop (nhds a)