Skip to content

Commit

Permalink
refactor(algebra/big_operators/order): use to_additive (#7173)
Browse files Browse the repository at this point in the history 
* 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.
  • Loading branch information
@urkud
urkud committed Apr 15, 2021
1 parent 5806a94 commit adfeb24
Show file tree
Hide file tree
Showing 2 changed files with 264 additions and 190 deletions.

0 comments on commit adfeb24

Please sign in to comment.