Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Group and Field Definitions


Jozef Bialas
Lodz University
Supported by RPBP.III-24.C9.

Summary.

The article contains exactly the same definitions of group and field as those in [4]. These definitions were prepared without the help of the definitions and properties of {\it Nat} and {\it Real} modes included in the MML. This is the first of a series of articles in which we are going to introduce the concept of the set of real numbers in a elementary axiomatic way.

MML Identifier: REALSET1

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

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[4] Jean Dieudonne. \em Foundations of Modern Analysis. Academic Press, New York and London, 1960.
[5] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. 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] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[9] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received October 27, 1989


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