# Zulip Chat Archive

## Stream: maths

### Topic: div_lt_iff_lt_mul

#### 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?

#### Kevin Buzzard (Jan 15 2019 at 11:26):

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

#### Mario Carneiro (Jan 15 2019 at 11:49):

it should be in `ordered_field`

somewhere

#### Mario Carneiro (Jan 15 2019 at 11:49):

`div_lt_iff`

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

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

#### Mario Carneiro (Jan 15 2019 at 12:21):

It's a theorem about fields because division

#### Mario Carneiro (Jan 15 2019 at 12:22):

division doesn't exist on monoids or groups

#### Kevin Buzzard (Jan 15 2019 at 12:22):

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

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

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

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