Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes