ideal.mul_le_right

Stream: maths

[Kevin Buzzard]

docs#ideal.mul_le_right says I * J ≤ I. Is that the correct convention?

[Chris Hughes]

I remember the convention is the opposite of what you'd expect. So I think that's the right way around. This isn't a very good way to remember the convention.

[Reid Barton]

It took me a while to figure out that this conversation was not about <=

[Eric Wieser]

docs#inf_le_right for comparison

[Eric Wieser]

The ideal one looks backwards to me

[Eric Wieser]

docs#nat.gcd_le_right also is the expected way around

[Kevin Buzzard]

I know there's a convention, I just don't know what the convention is :-)

[Eric Wieser]

I think the confusing one is a * b ≤ a * c