Partially ordered ring

In abstract algebra, a partially ordered ring is a ring ("A", +, ·), together with a "compatible partial order", i.e. a partial order formula_1 on the underlying set "A" that is compatible with the ring operations in the sense that it satisfies:
and
for all formula_7. Various extensions of this definition exist that constrain the ring, the partial order, or both. For example, an Archimedean partially ordered ring is a partially ordered ring formula_8 where formula_9's partially ordered additive group is Archimedean.
An ordered ring, also called a totally ordered ring, is a partially ordered ring formula_8 where formula_11 is additionally a total order.
An l-ring, or lattice-ordered ring, is a partially ordered ring formula_8 where formula_1 is additionally a lattice order.
Properties.
The additive group of a partially ordered ring is always a partially ordered group.
The set of non-negative elements of a partially ordered ring (the set of elements "x" for which formula_4, also called the positive cone of the ring) is closed under addition and multiplication, i.e., if "P" is the set of non-negative elements of a partially ordered ring, then formula_15 and formula_16. Furthermore, formula_17.
The mapping of the compatible partial order on a ring "A" to the set of its non-negative elements is one-to-one; that is, the compatible partial order uniquely determines the set of non-negative elements, and a set of elements uniquely determines the compatible partial order if one exists.
If "S" is a subset of a ring "A", and:
then the relation formula_1 where formula_2 iff formula_24 defines a compatible partial order on "A" ("ie." formula_8 is a partially ordered ring).
In any l-ring, the "absolute value" formula_26 of an element "x" can be defined to be formula_27, where formula_28 denotes the maximal element. For any "x" and "y",
holds.
f-rings.
An f-ring, or Pierce–Birkhoff ring, is a lattice-ordered ring formula_8 in which formula_31 and formula_32 imply that formula_33 for all formula_7. They were first introduced by Garrett Birkhoff and Richard S. Pierce in 1956, in a paper titled "Lattice-ordered rings", in an attempt to restrict the class of l-rings so as to eliminate a number of pathological examples. For example, Birkhoff and Pierce demonstrated an l-ring with 1 in which 1 is negative, even though it is a square. The additional hypothesis required of f-rings eliminates this possibility.
Example.
Let "X" be a Hausdorff space, and formula_35 be the space of all continuous, real-valued functions on "X". formula_35 is an Archimedean f-ring with 1 under the following pointwise operations:
From an algebraic point of view the rings formula_35
are fairly rigid. For example, localisations, residue rings or limits of rings of the form formula_35 are not of this form in general. A much more flexible class of f-rings containing all rings of continuous functions and resembling many of the properties of these rings, is the class of real closed rings.
Formally verified results for commutative ordered rings.
IsarMathLib, a library for the Isabelle theorem prover, has formal verifications of a few fundamental results on commutative ordered rings. The results are proved in the ring1 context.
Suppose formula_8 is a commutative ordered ring, and formula_7. Then: