Commit 2022-05-26 11:04 5aeafaab
View on Github →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.