∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G]
  {f : ℤ → G}, Function.Even f → Summable f → ∑' (n : ℤ), f n = f 0 + 2 • ∑' (n : ℕ+), f ↑↑n