Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
Submodules

Michal Muzalewski

Warsaw University, Bialystok
Summary.

This article contains the notions of trivial and
nontrivial leftmodules and rings, cyclic submodules and
inclusion of submodules. A few basic theorems related to these
notions are proved.
MML Identifier:
LMOD_6
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[2]
[11]
[12]
[1]
[7]
[3]
[10]
[9]
[8]
[4]
[5]

Preliminaries

Trivial and nontrivial modules and rings

Submodules and subsets

Cyclic submodules

Inclusion of left Rmodules
Bibliography
 [1]
Jozef Bialas.
Group and field definitions.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.
Abelian groups, fields and vector spaces.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Michal Muzalewski.
Free modules.
Journal of Formalized Mathematics,
3, 1991.
 [5]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Wojciech A. Trybulec.
Linear combinations in vector space.
Journal of Formalized Mathematics,
2, 1990.
 [9]
Wojciech A. Trybulec.
Operations on subspaces in vector space.
Journal of Formalized Mathematics,
2, 1990.
 [10]
Wojciech A. Trybulec.
Subspaces and cosets of subspaces in vector space.
Journal of Formalized Mathematics,
2, 1990.
 [11]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [12]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received June 19, 1992
[
Download a postscript version,
MML identifier index,
Mizar home page]