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

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.