Commit 2022-06-24 17:15 fe322e12

View on Github →

refactor(algebra/order/monoid): use typeclasses instead of lemmas (#14848) Use covariant_class/contravariant_class instead of type-specific mul_le_mul_left etc lemmas. Also, rewrite some proofs to use API about inequalities on with_top/with_bot instead of the exact form of the current definition.

Estimated changes

Modified src/algebra/order/monoid.lean

added theorem exists_one_lt_mul_of_lt

deleted theorem exists_pos_mul_of_lt

deleted theorem with_zero.lt_of_mul_lt_mul_left

deleted theorem with_zero.mul_le_mul_left

added theorem with_zero.zero_eq_bot

modified theorem with_zero.zero_le