Ordered ring: a ring with a total order compatible with addition and with positives closed under multiplication

An ordered ring is a ring $R$ (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides) together with a total order $\le$ on $R$ (Partial order and partially ordered set) such that, for all $a, b, c \in R$:

• (OR1) if $a \le b$ then $a + c \le b + c$;
• (OR2) if $0 < a$ and $0 < b$ then $0 < ab$.

As always $a < b$ means $a \le b$ and $a \ne b$. The positive cone of an ordered ring is

$P \;:=\; \{\, x \in R \;:\; 0 < x \,\},$

and its members are the positive elements. An element $x$ with $x < 0$ is negative. An ordered ring whose multiplication is commutative (Commutative ring) is an ordered commutative ring; nothing in the definition requires commutativity.

Convention, and the one place it differs from another in use. (OR2) is stated in the strict form: a product of two positive elements is positive. Some texts, and the Wikipedia article named below, instead require $0 \le a$ and $0 \le b$ to imply $0 \le ab$. Given (OR1) and a total order the two are not equivalent: the strict form is the non-strict one together with the extra requirement that a product of two positive elements is nonzero. The strict form is the one adopted here, for a reason internal to this library: it is verbatim what the published The integers form a totally ordered ring proves of $\mathbb{Z}$ ("$0 < x$ and $0 < y$ imply $0 < xy$") and verbatim what axiom (O2) of the published Ordered field requires of a positive cone, so with this convention both of those become instances of the present definition with nothing to adjust.

• Two presentations, one notion. An ordered ring may be presented by its order, as above, or by its positive cone, as Ordered field presents an ordered field. The order presentation and the positive-cone presentation of an ordered ring determine each other: $P = \{\, x : 0 < x \,\}$ satisfies trichotomy and closure, and $a < b :\iff b - a \in P$ recovers the order proves that the two presentations determine each other, so no second notion is introduced by the difference in style, and Every ordered field is an ordered ring, and its order is the one its positive cone induces is the bridge for fields.

• Both published order structures on this library's number systems are instances. $\mathbb{Z}$ with the order of Order on the integers is one, by The integers form a totally ordered ring; every ordered field is another, by Every ordered field is an ordered ring, and its order is the one its positive cone induces. The companion page records $\mathbb{Z}$, $\mathbb{Q}$ and $\mathbb{R}$ explicitly.

• The order is data. Writing "$R$ is an ordered ring" always means that a particular $\le$ has been fixed alongside the ring operations, exactly as "$F$ is an ordered field" fixes a particular positive cone in Ordered field. Nothing below depends on there being only one such order, and no uniqueness is claimed.