infinite_sum): generalize `tsum_le_of_sum_range_le` (#16951)

Commit

3 years ago

feat(topology/algebra/infinite_sum): generalize `tsum_le_of_sum_range_le` (#16951)

Author

kex-y

Parents