mathlib3

163ef61e - feat(topology/algebra/infinite_sum): add `tsum_star` (#13999)

feat(topology/algebra/infinite_sum): add `tsum_star` (#13999) These lemmas names are copied from `tsum_neg` and friends. As a result, `star_exp` can be golfed and generalized.