mathlib

adfeb249 - refactor(algebra/big_operators/order): use `to_additive` (#7173)

refactor(algebra/big_operators/order): use `to_additive` (#7173) * Replace many lemmas about `finset.sum` with lemmas about `finset.prod` + `@[to_additive]`; * Avoid `s \ t` in `finset.sum_lt_sum_of_subset`. * Use `M`, `N` instead of `α`, `β` for types with algebraic structures.