Commit 2025-08-28 17:04 22b83e98

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:

1. It's not clear that they should be iffs. In fact, the primed versions are not iffs!
2. The ₀ suffix to disambiguate from the ordered group lemmas isn't used. In fact, the primed versions are about ordered groups!
3. 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.