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.III-24.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 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]