From Wikipedia, the free encyclopedia
In abstract
algebra, an ordered ring is a commutative
ring R with a total order ≤ such that
for all a, b, and c in R:
- if a ≤ b then a + c ≤
b + c.
- if 0 ≤ a and 0 ≤ b then 0 ≤ ab.
Ordered rings are familiar from arithmetic. Examples include the real numbers. (The
rationals and reals in fact form ordered fields.) The complex numbers
do not form an ordered ring (or ordered field).
In analogy with real numbers, we call an element c ≠ 0,
of an ordered ring positive if 0 ≤ c and
negative if
c ≤ 0. 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:
where -a is the additive inverse of a and 0
is the additive identity element.
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:
- If a ≤ b and 0 ≤ c, then ac
≤ bc.^{[1]} This
property is sometimes used to define ordered rings instead of the
second property in the definition above.
- |ab| = |a| |b|.^{[2]}
- An ordered ring that is not trivial is infinite.^{[3]}
- Exactly one of the following is true: a is positive,
-a is positive, or a = 0.^{[4]} This
property follows from the fact that ordered rings are abelian, linearly ordered groups with respect to
addition.
- An ordered ring R has no zero divisors if and only if the positive
ring elements are closed under multiplication (i.e.
if a and b are positive, then so is
ab).^{[5]}
- In an ordered ring, no negative element is a square.^{[6]} This is
because if a ≠ 0 and a = b^{2}
then b ≠ 0 and a = (-b )^{2}; as
either b or -b is positive, a must be
positive.
Notes
The names below refer to theorems formally verified by the IsarMathLib project.
- ^
OrdRing_ZF_1_L9
- ^
OrdRing_ZF_2_L5
- ^
ord_ring_infinite
- ^
OrdRing_ZF_3_L2, see also OrdGroup_decomp
- ^
OrdRing_ZF_3_L3
- ^
OrdRing_ZF_1_L12