Commit 2025-09-10 16:44 16adc443

View on Github →

chore: swap mul_left_mono and mul_right_mono (#29396) mul_left_mono currently states monotonicity of left multiplication, ie right monotonicity of multiplication. There's ambiguity on which part of the sentence above should be followed in the name, but _mono/_strictMono lemmas are in large majority following the rule that it is "left/right monotonicity" that should be followed. See eg pow_left_mono, zsmul_left_mono. Unfortunately this means that the typeclass MulLeftMono corresponds to mul_right_mono. This could be fixed here or in a future PR.

Estimated changes

modified theorem mul_left_mono
modified theorem mul_left_strictMono
modified theorem mul_right_mono
modified theorem mul_right_strictMono
added theorem WithTop.coe_ne_one
modified theorem ENNReal.coe_ne_one
modified theorem ENNReal.coe_ne_zero
modified theorem ENNReal.mul_left_strictMono
modified theorem ENat.mul_left_strictMono
modified theorem ENat.mul_right_strictMono