Theorem is_sum_sum_of_ne_zero

feat(topology/infinite_sum): add tsum (with ∑ notation) and has_sum; add lemmas for different algebraic structures

feat(topology): introduce infinite sums on topological monoids