Commit 2020-06-26 13:39 6624509e
View on Github →feat(algebra/big_operators): telescoping sums (#3184) generalize sum_range_sub_of_monotone, a theorem about nats, to a theorem about commutative groups
feat(algebra/big_operators): telescoping sums (#3184) generalize sum_range_sub_of_monotone, a theorem about nats, to a theorem about commutative groups