Commit 2021-08-18 03:17 cb3d5db3

View on Github →

feat(algebra/ordered_monoid): generalize {min,max}mul_mul{left,right} (#8725) Before, it has assumptions about cancel_comm_monoid for all the lemmas. In fact, they hold under much weaker has_mul.

Estimated changes

Modified src/algebra/ordered_monoid.lean

modified theorem max_le_mul_of_one_le

modified theorem min_le_mul_of_one_le_left

modified theorem min_le_mul_of_one_le_right