mathlib3

8e522f85 - feat(algebra/order/monoid): Missing `has_exists_mul_of_le` instances (#14476)

feat(algebra/order/monoid): Missing `has_exists_mul_of_le` instances (#14476) Add a few `has_exists_mul_of_le` instances, generalize `has_exists_mul_of_le` to `has_le` + `has_mul`.