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 is a commutative ordered ring, and . Then:
| by | |
|---|---|
| The additive group of A is an ordered group | OrdRing_ZF_1_L4 |
| iff | OrdRing_ZF_1_L7 |
| and imply and |
OrdRing_ZF_1_L9 |
| ordring_one_is_nonneg | |
| OrdRing_ZF_2_L5 | |
| ord_ring_triangle_ineq | |
| x is either in the positive set, equal to 0, or in minus the positive set. | OrdRing_ZF_3_L2 |
| The set of positive elements of is closed under multiplication iff A has no zero divisors. | OrdRing_ZF_3_L3 |
| If A is non-trivial, then it is infinite. | ord_ring_infinite |
Read more about this topic: Partially Ordered Ring
Famous quotes containing the words formally, verified, results, ordered and/or rings:
“We find the most terrible form of atheism, not in the militant and passionate struggle against the idea of God himself, but in the practical atheism of everyday living, in indifference and torpor. We often encounter these forms of atheism among those who are formally Christians.”
—Nicolai A. Berdyaev (1874–1948)
“Essential truth, the truth of the intellectualists, the truth with no one thinking it, is like the coat that fits tho no one has ever tried it on, like the music that no ear has listened to. It is less real, not more real, than the verified article; and to attribute a superior degree of glory to it seems little more than a piece of perverse abstraction-worship.”
—William James (1842–1910)
“I have no doubt that it was a principle they fought for, as much as our ancestors, and not to avoid a three-penny tax on their tea; and the results of this battle will be as important and memorable to those whom it concerns as those of the battle of Bunker Hill, at least.”
—Henry David Thoreau (1817–1862)
“Your mind was wrought in cosmic solitude,
Through which careered an undulous pageantry
Of fiends and suns, darkness and boiling sea,
All held in ordered sway by beauty’s mood.”
—Allen Tate (1899–1979)
“It is told that some divorcees, elated by their freedom, pause on leaving the courthouse to kiss a front pillar, or even walk to the Truckee to hurl their wedding rings into the river; but boys who recover the rings declare they are of the dime-store variety, and accuse the throwers of fraudulent practices.”
—Administration in the State of Neva, U.S. public relief program. Nevada: A Guide to the Silver State (The WPA Guide to Nevada)