mathlib

5aeafaab - feat(algebra/order/monoid): add `le_iff_exists_mul'` (#14387)

feat(algebra/order/monoid): add `le_iff_exists_mul'` (#14387) Add a version of `le_iff_exists_mul'`/`le_iff_exists_add'`, versions of `le_iff_exists_mul`/`le_iff_exists_add` with multiplication on the other side.