Commit 2023-02-08 20:27 cd424234

feat(topology/algebra/infinite_sum): add tsum_finset_bUnion_disjoint (#18350) This is the n-ary version of tsum_union_disjoint, although unfortunately I realized that what I actually wanted was the n-ary version of has_sum.add_is_compl which is harder to state! Either way, this lemma seems worth having.