div_lt_iff_lt_mul

Stream: maths

[Kevin Buzzard]

I just wanted to get from a<b*c to a/c<b (on the real numbers) with a hypothesis that c>0. I was surprised to find that although all three of div_lt_iff_lt_mul, lt_mul_of_div_lt and div_lt_of_lt_mul were in Lean, they were in data.int.basic :-) and only applied to ints. This should be some general lemma about ordered monoids or some such thing, right? I might start doing what Chris always encourages me to do, which is to make a super-short PR, assuming that this is actually something missing from mathlib. But is it there and I missed it?

[Kevin Buzzard]

Currently struggling to find ordered monoids :-/ Do we only have ordered additive monoids?

[Mario Carneiro]

it should be in ordered_field somewhere

[Mario Carneiro]

div_lt_iff

[Mario Carneiro]

lean core has several more long winded unidirectional versions - div_lt_of_mul_lt_of_pos , I can't find the reverse direction

[Kevin Buzzard]

Aah! This is a theorem about multiplication and 0 (which is to do with addition) so indeed it's not about monoids. Maybe it's about ordered semirings? Thanks Mario.

[Mario Carneiro]

It's a theorem about fields because division

[Mario Carneiro]

division doesn't exist on monoids or groups

[Kevin Buzzard]

Oh of course. ok it all makes sense now :-)

[Kevin Buzzard]

Now I'm just annoyed that I didn't go through this thought process myself before asking.

[Kevin Buzzard]

Had I taken the trouble to try and formalise what statement I thought was true for ordered monoids I suspect I would have made more progress on my own...

[Mario Carneiro]

you might wonder why division isn't defined for groups, and this is one of the differences from add_groups, which have subtraction, but there is a difference between the total division on groups and the almost total division on fields and it doesn't seem to be helpful to unify them; lots of theorems overlap with a name conflict, but they are all proven differently