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


This paper contains the second part of the set of articles concerning the theory of algebraic structures, based on [4, pp. 9-12] (pages 4-6 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 quasi-field, right quasi-field, double sided quasi-field, 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.III-24.B5.

MML Identifier: ALGSTR_2

The terminology and notation used in this paper have been introduced in the following articles [5] [1] [2] [3]

Contents (PDF format)


[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 bi-modules 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]