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

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.III24.C6.
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)
Bibliography
 [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 bimodules 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]