# Zulip Chat Archive

## Stream: maths

### Topic: Definition of ordered rings

#### Christopher Hoskin (Jan 13 2021 at 15:29):

There seems to me to be something unsatisfactory about the mathlib definition of a (partially) ordered ring [1]. Specifically, it seems to me that

```
(mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
```

ought to be

```
(mul_pos : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b)
```

This is the axiom used in other locations e.g. [2], [3], [4]. More importantly the space of continuous real-valued functions on the unit interval is not an ordered ring according to the mathlib definition. (Consider two bump functions with disjoint supports.) Should we not expect a useful definition of ordered ring to include continuous bounded functions on a locally compact Hausdorff space?

Is there a reason `mul_pos`

is specified the way it is?

Thanks,

Christopher

[1] https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ordered_ring.lean#L490-L492

[2] https://en.wikipedia.org/wiki/Ordered_ring

[3] https://isabelle.in.tum.de/library/HOL/HOL/Rings.html

[4] https://www.google.co.uk/books/edition/Lecture_Notes_On_Algebraic_Structure_Of/6vq2CgAAQBAJ?hl=en&gbpv=1&dq=ordered+rings&pg=PA20&printsec=frontcover

#### Damiano Testa (Jan 13 2021 at 15:32):

Just from a naming point of view, wouldn't your suggestion be called `mul_nonneg`

?

#### Damiano Testa (Jan 13 2021 at 15:33):

https://leanprover-community.github.io/mathlib_docs/algebra/ordered_ring.html#mul_nonneg

#### Mario Carneiro (Jan 13 2021 at 15:34):

I think we just put the strongest properties we could get away with; there is a whole zoo of less constrained algebraic objects and it would be a lot of navel gazing to explore all of them, so we're just adding them as they become required for applications

#### Mario Carneiro (Jan 13 2021 at 15:35):

For conventional rings like `int`

(or totally ordered rings more generally) it's no problem to have a rule like `mul_pos`

#### Mario Carneiro (Jan 13 2021 at 15:36):

it's certainly a theorem you want to be true in "some generality", so we need a class to represent it and the theorems that derive from it anyway

#### Reid Barton (Jan 13 2021 at 15:38):

I think linearly ordered rings should probably have this `mul_pos`

property, but not general ordered rings

#### Mario Carneiro (Jan 13 2021 at 15:38):

I recall us investigating this a while ago. In fact I suspect the definition did not have mul_pos in it two years ago

#### Reid Barton (Jan 13 2021 at 15:39):

There was some discussion about related topics back in October (#4296, #4363) but I'm not sure about this specifically

#### Mario Carneiro (Jan 13 2021 at 15:42):

Ah yeah that was what I was thinking of

#### Mario Carneiro (Jan 13 2021 at 15:42):

from what I can tell this rule dates back at least to when `ordered_ring`

was in core

#### Bryan Gin-ge Chen (Jan 13 2021 at 16:21):

The fact that mathlib's definition doesn't agree with other standard sources and there's no mention of it in the doc string is a problem. We could of course just add a doc string with a possible `TODO`

for a bigger refactor.

#### Eric Wieser (Jan 13 2021 at 16:47):

Just as an exercises, these two definitions are equivalent if `[no_zero_divisors R]`

is around:

```
example {R : Type*} [ring R] [partial_order R] :
(∀ a b : R, 0 < a → 0 < b → 0 < a * b) → (∀ a b : R, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) :=
begin
intros h a b ha hb,
by_cases haz : a = 0,
{ rw [haz, zero_mul], },
by_cases hbz : b = 0,
{ rw [hbz, mul_zero], },
have ha' := or.resolve_right (le_iff_lt_or_eq.mp ha) (ne.symm haz),
have hb' := or.resolve_right (le_iff_lt_or_eq.mp hb) (ne.symm hbz),
exact le_of_lt (h _ _ ha' hb'),
end
-- needed for the reverse direction
example {R : Type*} [ring R] [partial_order R] [no_zero_divisors R]:
(∀ a b : R, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) → (∀ a b : R, 0 < a → 0 < b → 0 < a * b) :=
begin
intros h a b ha hb,
cases le_iff_lt_or_eq.mp (h _ _ (le_of_lt ha) (le_of_lt hb)) with h1 h2,
{ exact h1, },
exfalso,
exact (eq_zero_or_eq_zero_of_mul_eq_zero h2.symm).rec (ne_of_gt ha) (ne_of_gt hb),
end
```

#### Mario Carneiro (Jan 13 2021 at 17:29):

In the isabelle version, it looks like `mul_pos`

is derived from `mul_nonneg`

over a total order. If that works that seems fine to me

#### Mario Carneiro (Jan 13 2021 at 17:30):

oh but you have to assume `0 < 1`

#### Johan Commelin (Jan 13 2021 at 17:38):

which also make sense, I guess

#### Christopher Hoskin (Jan 13 2021 at 18:00):

@Damiano Testa From an Operator Algebra point of view, I'd use the term "positive" for "0 ≤ " and "strictly positive" for "0<". But that might not match Mathlib's conventions.

#### Floris van Doorn (Jan 13 2021 at 18:36):

Currently the only instance of `ordered_ring`

in mathlib that is not linearly ordered is docs#filter.germ.ordered_ring. I think it would be good to change our definition to the standard definition.

Last updated: May 10 2021 at 07:15 UTC