mathlib3

adb6142d - refactor(topology/algebra/infinite_sum): generalize `tsum_zero` (#15786)

refactor(topology/algebra/infinite_sum): generalize `tsum_zero` (#15786) Thanks to @kbuzzard and @b-mehta, it holds whenever `is_closed {0}`. This is true not just as `t2_space` as before, but in all `t1_space`.