Commit 2023-01-19 10:30 b84da9c8

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.