mathlib3

766146b9 - fix(topology/algebra/infinite_sum): remove hard-coding of ℕ and ℝ (#6096)

fix(topology/algebra/infinite_sum): remove hard-coding of ℕ and ℝ (#6096) It may be possible to make these assumptions stricter, but they're weak enough to still cover the original use case. Hopefully that can be handled by @alexjbest's upcoming linter to relax assumptions.