Commit 2025-08-28 17:04 22b83e98
View on Github →chore: rename mul_le_mul_left
/mul_le_mul_right
to mul_le_mul_iff_right₀
/mul_le_mul_iff_left₀
(#28645)
This is one of the longest standing naming issues in mathlib.
The issues with the existing names are:
- It's not clear that they should be iffs. In fact, the primed versions are not iffs!
- The
₀
suffix to disambiguate from the ordered group lemmas isn't used. In fact, the primed versions are about ordered groups! - The
_left
/_right
convention used isn't so clear. With the new names, it is very clear:_iff_left
means that the RHS of the iff refers to the variables left of the multiplication on the LHS.