le_mul_left

Stream: mathlib4

[Violeta Hernández]

docs#Ordinal.le_mul_left is 0 < b → a ≤ a * b while docs#Cardinal.le_mul_left is b ≠ 0 → a ≤ b * a.

[Violeta Hernández]

Which one is "correct"?

[Violeta Hernández]

I'm inclined to say that either the left is the correct one, or that it's actually a mix of both b ≠ 0 → a ≤ a * b.

[Violeta Hernández]

Oh and to make matters worse, a is explicit in the former but implicit in the latter

[Violeta Hernández]

I have no preference there, but I'd still like these theorems to be consistent with each other

[Eric Wieser]

docs#Nat.le_mul_of_pos_left is some other precedence

[Bhavik Mehta]

Annoyingly docs#le_mul_left is some other statement!

[Violeta Hernández]

Hm, should both of these statements be renamed to le_mul_of_pos_left and made to match the Nat statement then?

[Eric Wieser]

docs#le_mul_of_one_le_left' seems to be the general spelling