mathlib

65c9ffb2 - feat(topology/algebra/infinite_sum) Sums over Z vs sums over N (#14667)

feat(topology/algebra/infinite_sum) Sums over Z vs sums over N (#14667) This PR adds some functions for handling infinite sums indexed by the integers, relating them to sums over the naturals.