mathlib3

fc640963 - feat(topology/algebra/infinite_sum): summable on subtype iff (#14032)

feat(topology/algebra/infinite_sum): summable on subtype iff (#14032) A summable version of the `has_sum` lemma previously (the `tsum` version is already present) Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>