mathlib3

b84da9c8 - feat(topology/algebra/infinite_sum): Generalized lemmas for `add_comm_monoid` rather than `add_comm_group` (#17035)

feat(topology/algebra/infinite_sum): Generalized lemmas for `add_comm_monoid` rather than `add_comm_group` (#17035) This PR adds generalized (but weaker) versions of `has_sum.update`, `has_sum.ite_eq_extract`, and `tsum_ite_eq_extract` when the co-domain is a monoid rather than a group. The main use of this is with `nnreal` and `ennreal`, to write things like a `tsum` over an `option` type as a sum of the `none` and `some` cases separately.