mathlib

16320e2e - chore(topology/algebra/infinite_sum): refactor `tsum_mul_left/right` (#5533)

chore(topology/algebra/infinite_sum): refactor `tsum_mul_left/right` (#5533) * move old lemmas to `summable` namespace; * add new `tsum_mul_left` and `tsum_mul_right` that work in a `division_ring` without a `summable` assumption.