[Merged by Bors] - feat(algebra/ordered_ring): ask for 0 < 1 earlier.

[semorrison]

It used to be that linear_ordered_semiring asked for 0 < 1, while ordered_semiring didn't.

I'd prefer that ordered_semiring asks for this already:

1. because lots of interesting examples (e.g. rings of operators) satisfy this property
2. because the rest of mathlib doesn't care

---

(In fact, I think it would be good to weaken this to only ask for 0 ≤ 1, and use [nontrivial] to obtain 0 < 1 when necessary, but I don't want to try that yet.)

I know nothing about the abstract theory of ordered rings, so if someone has any reason to object to this, no problem! As an alternative I can make separate typeclasses: one that says 0 ≤ 1, and another that says the ordering is linear. However we already have far too many classes in the order hierarchy, so unless someone actually cares about ordered rings without 0 ≤ 1, let's not even admit them to the discussion!

Blocked by #4295.

[gebner]

I don't see an issue with moving the 0 < 1 to ordered semirings or making it 0 ≤ 1.

[robertylewis]

Looks fine to me, and I also don't see any issues. @digama0 @kbuzzard any reason to object to this?

[digama0]

One objection I have is that this makes unit not an ordered semiring, nor the semiring defined from a canonically ordered add_monoid with always-zero multiplication. It seems vaguely bad to me, but I don't know whether it's just like the 0 != 1 constraint in domains (which seems unnecessary for what it does but is common in traditional maths). But since we aren't really using this property in mathlib, I'm fine with going ahead with this if it's convenient for some formalization purpose; if we need the other one later we'll battle out the naming then.

[robertylewis]

If there's a later refactor to weaken this to <= then unit will be an ordered semiring again.

[semorrison]

Yes, I would like to weaken this to <=, but as it seems like no one needs this immediately I'd prefer to do it in stages.

[semorrison]

On the other hand the current change actually has a mathematical significance: I have a branch with Bell's inequality and Tsirelson's inequality (about nonlocality in quantum mechanics). Typically these are either proved "in physics" or in the setting of C^*-algebras, but once ordered_ring has 0 \le 1 I can give a purely *-algebraic formulation and proof.

[gebner]

Ok, so we all agree that this is the way to go. We're looking forward to the 0 ≤ 1 PR.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests

[kbuzzard]

Three weeks too late -- I don't have a problem with this. I have no opinion on whether the trivial ring is ordered.