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

Groups, Rings, Left- and Right-Modules

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


The notion of group was defined as a group structure introduced in the article [1]. The article contains the basic properties of groups, rings, left- and right-modules of an associative ring.

Supported by RPBP.III-24.C6.

MML Identifier: MOD_1

The terminology and notation used in this paper have been introduced in the following articles [3] [1] [2]

Contents (PDF format)


[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] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

Received October 22, 1990

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