Commit 2021-12-26 23:49 7c9ce5c0
View on Github →feat(algebra/order/monoid_lemmas): mul_eq_mul_iff_eq_and_eq (#11056)
If a ≤ c and b ≤ d, then a * b = c * d iff a = c and b = d.
feat(algebra/order/monoid_lemmas): mul_eq_mul_iff_eq_and_eq (#11056)
If a ≤ c and b ≤ d, then a * b = c * d iff a = c and b = d.