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

Jozef Bialas

University of Lodz

Supported by RPBP.III24.C9.
Summary.

The second part of considerations concerning
groups and fields. It includes a definition and properties of
commutative field $F$ as a structure defined by: the set, a support
of $F$, containing
two different elements, by two binary operations
${\bf +}_{F}$, ${\bf \cdot}_{F}$ on this
set, called addition and multiplication, and by two elements from
the support of $F$,
${\bf 0}_{F}$ being neutral for addition and
${\bf 1}_{F}$ being neutral for
multiplication. This structure is named a field if
$\langle$the support of $F$, ${\bf +}_{F}$, ${\bf 0}_{F} \rangle$
and
$\langle$the support of $F$, ${\bf \cdot}_{F}$, ${\bf 1}_{F} \rangle$
are commutative groups and multiplication
has the property of lefthand and righthand distributivity with respect to
addition. It is demonstrated that the field $F$ satisfies the definition of
a field in the axiomatic approach.
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[4]
[8]
[9]
[2]
[3]
[7]
[5]
[1]
Contents (PDF format)
Bibliography
 [1]
Jozef Bialas.
Group and field definitions.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [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 June 20, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]