Summation in topological groups

Summary

Let $(x_i)_{i \in I}$ be a family in a commutative topological group, indexed by any set $I$. It has sum $s$ when the finite partial sums $\sum_{i \in F} x_i$ converge to $s$ as the finite set $F \subseteq I$ grows. This defines infinite sums with no order on the index set, and the sum does not depend on any rearrangement. In a Hausdorff group a family has at most one sum. This is the notion of summability used in Mathlib (HasSum), and it covers series in $\R$, in Banach spaces and in $p$-adic numbers.