Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

The Ring of Integers, Euclidean Rings and Modulo Integers


Christoph Schwarzweller
University of T\"ubingen

Summary.

In this article we introduce the ring of Integers, Euclidean rings and Integers modulo $p$. In particular we prove that the Ring of Integers is an Euclidean ring and that the Integers modulo $p$ constitutes a field if and only if $p$ is a prime.

MML Identifier: INT_3

The terminology and notation used in this paper have been introduced in the following articles [15] [20] [2] [16] [18] [21] [5] [6] [13] [10] [12] [4] [9] [8] [14] [17] [3] [7] [11] [1] [19]

Contents (PDF format)

  1. The Ring of Integers
  2. Euclidean Rings
  3. Some Theorems about Div and Mod
  4. Modulo Integers

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.
[4] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Journal of Formalized Mathematics, 3, 1991.
[8] Agata Darmochwal. The Euclidean space. Journal of Formalized Mathematics, 3, 1991.
[9] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.
[10] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[11] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.
[12] Michal Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Journal of Formalized Mathematics, 2, 1990.
[13] Christoph Schwarzweller. The correctness of the generic algorithms of Brown and Henrici concerning addition and multiplication in fraction fields. Journal of Formalized Mathematics, 9, 1997.
[14] Dariusz Surowik. Cyclic groups and some of their properties --- part I. Journal of Formalized Mathematics, 3, 1991.
[15] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[16] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[17] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[18] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[19] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.
[20] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[21] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received February 4, 1999


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