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:

  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.

Estimated changes