monoid_lemmas): `mul_eq_mul_iff_eq_and_eq` (#11056)

Commit

3 years ago

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

Author

tb65536

Parents