Commit 2024-08-11 05:10 ce6b0a98

refactor: Unify the different versions of mul_eq_one (#14996) Replace mul_eq_one_iff and Associates.mul_eq_one_iff by a single lemma mul_eq_one. Rename mul_eq_one_iff' to mul_eq_one_iff_of_one_le. Similarly for the additive versions.