mathlib
6624509e - feat(algebra/big_operators): telescoping sums (#3184)

Commit

5 years ago

feat(algebra/big_operators): telescoping sums (#3184) generalize sum_range_sub_of_monotone, a theorem about nats, to a theorem about commutative groups

Author

jalex-stark

Parents

5b97da63

mathlib 6624509e - feat(algebra/big_operators): telescoping sums (#3184)

mathlib
6624509e - feat(algebra/big_operators): telescoping sums (#3184)