Zulip Chat Archive

Stream: maths

Topic: div_lt_iff_lt_mul


view this post on Zulip Kevin Buzzard (Jan 15 2019 at 11:21):

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?

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 11:26):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 11:49):

it should be in ordered_field somewhere

view this post on Zulip Mario Carneiro (Jan 15 2019 at 11:49):

div_lt_iff

view this post on Zulip Mario Carneiro (Jan 15 2019 at 11:52):

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

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 12:15):

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.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:21):

It's a theorem about fields because division

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:22):

division doesn't exist on monoids or groups

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 12:22):

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

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 12:22):

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

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 12:23):

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...

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:24):

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


Last updated: May 18 2021 at 08:14 UTC