mathlib3

6ef05bb3 - feat(topology/algebra/infinite_sum): infinite sums on subsets (#16671)

feat(topology/algebra/infinite_sum): infinite sums on subsets (#16671) * Add more lemmas about infinite sums on subsets of the domain * Group some existing lemmas together in the same "section" * Also add some lemmas about `set.maps_to.restrict` that I used until I refactored one of the proofs