Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
From Double Loops to Fields

Wojciech Skaba

Torun University

Michal Muzalewski

Warsaw University, Bialystok
Summary.

This paper contains the second part of the set of articles
concerning the theory of algebraic structures, based on [4, pp. 912]
(pages 46 of the English edition).\par
First the basic structure $\langle F, +, \cdot, 1, 0\rangle$ is defined. Following it
the consecutive structures are contemplated in details, including
double loop, left quasifield, right quasifield, double sided quasifield,
skew field and field. These structures are created by gradually
augmenting the basic structure with new axioms of commutativity,
associativity, distributivity etc.
Each part of the article begins with the set of auxiliary theorems
related to the structure under consideration, that are necessary
for the existence proof of each defined mode. Next the mode and proof
of its existence is included. If the current set of axioms may be
replaced with a different and equivalent one, the appropriate proof
is performed following the definition of that mode.
With the introduction of double loop the ``'' function is defined.
Some interesting features of this function are also included.
Supported by RPBP.III24.B5.
The terminology and notation used in this paper have been
introduced in the following articles
[5]
[1]
[2]
[3]
Contents (PDF format)
Bibliography
 [1]
Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.
Abelian groups, fields and vector spaces.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Michal Muzalewski.
Construction of rings and left, right, and bimodules over a ring.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Michal Muzalewski and Wojciech Skaba.
From loops to abelian multiplicative groups with zero.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Wanda Szmielew.
\em From Affine to Euclidean Geometry, volume 27.
PWN  D.Reidel Publ. Co., Warszawa  Dordrecht, 1983.
 [5]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
Received September 27, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]