mathlib3

cb3d5db3 - feat(algebra/ordered_monoid): generalize {min,max}_mul_mul_{left,right} (#8725)

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`.