Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
Ordered Rings  Part II

Michal Muzalewski

Warsaw University, Bialystok

Leslaw W. Szczerba

Siedlce University
Summary.

This series of papers is devoted to the notion of the ordered ring,
and one of its most important cases: the notion of ordered field. It
follows the results of [5]. The idea of the notion of
order in the ring is based on that of
positive cone i.e. the set of positive elements. Positive cone has to
contain at least squares of all elements, and has to be closed under sum
and product. Therefore the key notions of this theory are that of square,
sum of squares, product of squares, etc. and finally elements generated
from squares by means of sums and products. Part II contains
classification of sums of such elements.
The terminology and notation used in this paper have been
introduced in the following articles
[2]
[1]
[6]
[3]
[4]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.
Abelian groups, fields and vector spaces.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Michal Muzalewski and Leslaw W. Szczerba.
Ordered rings  part I.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Wanda Szmielew.
\em From Affine to Euclidean Geometry, volume 27.
PWN  D.Reidel Publ. Co., Warszawa  Dordrecht, 1983.
 [6]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
Received October 11, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]