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. 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

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 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.