Commit 2023-08-10 08:49 35ae7708
View on Github →chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier (#6483)
This move was suggested in #6220. In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was.
Affected files:
Algebra.Group.UniqueProds
Algebra.Order.Monoid.Basic