Ordered ring

In abstract algebra, an ordered ring is a (usually commutative) ring "R" with a total order ≤ such that for all "a", "b", and "c" in "R":
Examples.
Ordered rings are familiar from arithmetic. Examples include the integers, the rationals and the real numbers. (The rationals and reals in fact form ordered fields.) The complex numbers, in contrast, do not form an ordered ring or field, because there is no inherent order relationship between the elements 1 and "i".
Positive elements.
In analogy with the real numbers, we call an element "c" of an ordered ring "R" positive if 0 < "c", and negative if "c" < 0. 0 is considered to be neither positive nor negative.
The set of positive elements of an ordered ring "R" is often denoted by "R"+. An alternative notation, favored in some disciplines, is to use "R"+ for the set of nonnegative elements, and "R"++ for the set of positive elements.
Absolute value.
If formula_1 is an element of an ordered ring "R", then the absolute value of formula_2, denoted formula_3, is defined thus:
where formula_5 is the additive inverse of formula_2 and 0 is the additive identity element.
Discrete ordered rings.
A discrete ordered ring or discretely ordered ring is an ordered ring in which there is no element between 0 and 1. The integers are a discrete ordered ring, but the rational numbers are not.
Basic properties.
For all "a", "b" and "c" in "R":
Notes.
The list below includes references to theorems formally verified by the IsarMathLib project.