In Abstract_algebra, an '''ordered ring''' is a Commutative_ring $R$ with a Total_order $\backslash leq$ such that * if $a\backslash leq\; b$ and $c\backslash in\; R$, then $a+c\; \backslash leq\; b+c$ * if $0\; \backslash leq\; a$ and $0\backslash leq\; b$, then $0\; \backslash leq\; ab$. 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). In analogy with ordinary numbers, we call an element ''c'' of an ordered ring '''positive''' if $0\backslash leq\; c,\; c\backslash neq\; 0$ and '''negative''' if $c\backslash leq\; 0,\; c\backslash neq0$. 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. == Basic properties == *If $a\backslash leq\; b$ and $0\backslash leq\; c$, then $ac\backslash leq\; bc.${{ref|ineq}} This property is sometimes used to define ordered rings instead of the second property in the definition above. *If $a,b\; \backslash in\; R$, then $|ab|=|a||b|.${{ref|abs}} *An ordered ring that is not trivial is infinite. {{ref|inf}} *If $a\backslash in\; R$, then either $a\backslash in\; R\_+$, or $-a\; \backslash in\; R\_+$, or $a=0\backslash ,.${{ref|partition}} 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 $R\_+$ is closed under multiplication—that is, $ab$ is positive if both $a$ and $b$ are positive.{{ref|equiv}} *In an ordered ring, no negative element is a square.{{ref|square}} This is because if $a\backslash neq\; 0$ and $a=b^2$ then $b\backslash neq\; 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. #{{note|ineq}} OrdRing_ZF_1_L9 #{{note|abs}} OrdRing_ZF_2_L5 #{{note|inf}} ord_ring_infinite #{{note|partition}} OrdRing_ZF_3_L2, see also OrdGroup_decomp #{{note|equiv}} OrdRing_ZF_3_L3 #{{note|square}} OrdRing_ZF_1_L12 Category:Ordered_groups Ca:Anell_ordenat Es:Anillo_ordenado Pl:Pierścień_uporządkowany