Commit 2024-08-19 07:42 80afba9b

feat: generalise mul_eq_one etc. to cancellative monoids (#15921) More specifically eq_one_of_mul_right, eq_one_of_mul_left, mul_eq_one and a new simple corollary mul_ne_one. The [Left|Right]CancelMonoid versions are protected and the CancelMonoid versions are primed. This is part of #15864. Note that these theorems cannot be generalised to [Monoid α] – see https://math.stackexchange.com/a/4535529/357390 for a counterexample monoid.