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)
“To regard the successful experiences which ensue from a belief as a criterion of its truth is one thing—and a thing that is sometimes bad and sometimes good—but to assume that truth itself consists in the process by which it is verified is a different thing and always bad.”
—William Pepperell Montague (1842–1910)
“It is perhaps the principal admirableness of the Gothic schools of architecture, that they receive the results of the labour of inferior minds; and out of fragments full of imperfection ... raise up a stately and unaccusable whole.”
—John Ruskin (1819–1900)
“The peace conference must not adjourn without the establishment of some ordered system of international government, backed by power enough to give authority to its decrees. ... Unless a league something like this results at our peace conference, we shall merely drop back into armed hostility and international anarchy. The war will have been fought in vain ...”
—Virginia Crocheron Gildersleeve (1877–1965)
“Ah, Christ, I love you rings to the wild sky
And I must think a little of the past:
When I was ten I told a stinking lie
That got a black boy whipped....”
—Allen Tate (1899–1979)