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

From Loops to Abelian Multiplicative Groups with Zero

Michal Muzalewski
Warsaw University, Bialystok
Wojciech Skaba
Nicolaus Copernicus University, Torun


Elementary axioms and theorems on the theory of algebraic structures, taken from the book [5]. First a loop structure $\langle G, 0, +\rangle$ is defined and six axioms corresponding to it are given. Group is defined by extending the set of axioms with $(a+b)+c = a+(b+c)$. At the same time an alternate approach to the set of axioms is shown and both sets are proved to yield the same algebraic structure. A trivial example of loop is used to ensure the existence of the modes being constructed. A multiplicative group is contemplated, which is quite similar to the previously defined additive group (called simply a group here), but is supposed to be of greater interest in the future considerations of algebraic structures. The final section brings a slightly more sophisticated structure i.e: a multiplicative loop/group with zero: $\langle G, \cdot, 1, 0\rangle$. Here the proofs are a more challenging and the above trivial example is replaced by a more common (and comprehensive) structure built on the foundation of real numbers.

Supported by RPBP.III-24.C6.

MML Identifier: ALGSTR_1

The terminology and notation used in this paper have been introduced in the following articles [6] [9] [7] [1] [2] [8] [4] [3]

Contents (PDF format)


[1] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[3] Michal Muzalewski. Midpoint algebras. Journal of Formalized Mathematics, 1, 1989.
[4] Michal Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. 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] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[7] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[8] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[9] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received July 10, 1990

[ Download a postscript version, MML identifier index, Mizar home page]