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:
“From a bed in this hotel Seargent S. Prentiss arose in the middle of the night and made a speech in defense of a bedbug that had bitten him. It was heard by a mock jury and judge, and the bedbug was formally acquitted.”
—Federal Writers’ Project Of The Wor, U.S. public relief program (1935-1943)
“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)
“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)
“Today everything is different. I can’t even get decent food. Right after I got here I ordered some spaghetti with marinara sauce and I got egg noodles and catsup. I’m an average nobody, I get to live the rest of my life like a schnook.”
—Nicholas Pileggi, U.S. screenwriter, and Martin Scorsese. Henry Hill (Ray Liotta)
“We will have rings and things, and fine array,
And kiss me, Kate, we will be married o’ Sunday.”
—William Shakespeare (1564–1616)