Definitions

In abstract algebra, an ordered ring is a commutative ring R with a a total order such that Abstract algebra is the field of mathematics concerned with the study of algebraic structures such as groups, rings and fields. ... In ring theory, a branch of abstract algebra, a commutative ring is a ring in which the multiplication operation obeys the commutative law. ... In mathematics, a total order, linear order or simple order on a set X is any binary relation on X that is antisymmetric, transitive, and total. ...

• if and , then

• if and , then .

Ordered rings are familiar from arithmetic. Examples include the integers, the rational numbers, and the real numbers. (The rationals and reals in fact form ordered fields.) The complex numbers do not form an ordered ring (or field). Arithmetic or arithmetics (from the Greek word αριθμός = number) in common usage is a branch of (or the forerunner of) mathematics which records elementary properties of certain operations on numerals, though in usage by professional mathematicians, it often is treated as a synonym for number theory. ... The integers consist of the positive natural numbers (1, 2, 3, …) the negative natural numbers (−1, −2, −3, ...) and the number zero. ... In mathematics, a rational number (or informally fraction) is a ratio or quotient of two integers, usually written as the vulgar fraction a/b, where b is not zero. ... In mathematics, the real numbers are intuitively defined as numbers that are in one-to-one correspondence with the points on an infinite line—the number line. ... In mathematics, an ordered field is a field (F,+,*) together with a total order ≤ on F that is compatible with the algebraic operations in the following sense: if a ≤ b then a + c ≤ b + c if 0 ≤ a and 0 ≤ b then 0 ≤ a b It follows from these axioms... In mathematics, a complex number is an expression of the form a + bi, where a and b are real numbers, and i stands for the square root of minus one (−1), which cannot be represented by any real number. ...

In analogy with ordinary numbers, we call an element c of an ordered ring positive if and negative if . The set of positive (or, in some cases, nonnegative) elements in the ring R is often denoted by R ₊ .

If a is an element of an ordered ring R, then the absolute value of a, denoted | a | , is defined thus: In mathematics, the absolute value (or modulus1) of a real number is its numerical value without regard to its sign. ...

,

where − a is the additive inverse of a and 0 is the additive identity element. The additive inverse, or opposite, of a number n is the number which, when added to n, yields zero. ... In mathematics, an identity element (or neutral element) is a special type of element of a set with respect to a binary operation on that set. ...

Basic properties

The names in parentheses below refer to the theorems formally verified by the IsarMathLib project.

1. If and , then (OrdRing_ZF_2_L8). This property is sometimes used to define ordered rings instead of the second property in the definition above.
2. If , then | ab | = | a | | b | (OrdRing_ZF_2_L5).
3. If , then either , or , or (OrdRing_ZF_3_L2). This property follows from the fact that ordered rings are abelian, linearly ordered groups with respect to addition.
4. If the ring R has no zero divisors, then R ₊ is closed under multiplication—that is, ab is positive if both a and b are positive (OrdRing_ZF_3_L3).