feat: convergence of infinite sums in nonarchimedean abelian groups

[trivial1711]

Let G be a complete nonarchimedean abelian group and let f : α → G be a function. We prove that f is unconditionally summable if and only if f a tends to zero on the cofinite filter on α.

---

[trivial1711]

One question I have for the reviewers is what folder this file should be in (Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean, or Mathlib.Topology.Algebra.Nonarchimedean.InfiniteSum?) . The other is what namespace the theorems should be in (NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero, or summable_iff_tendsto_cofinite_zero?).

[trivial1711]

I made this proof more complicated than it needs to be. I can simplify it by using cauchySeq_finset_iff_vanishing. I will work on this.

[trivial1711]

Thank you for the review. I have made the changes you suggest.

[fpvandoorn]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style