The Chinese Remainder Theorem

Andrzej Kondracki

AMS Management Systems Poland, Warsaw

Summary.

The article is a translation of the first chapters of a book {\em Wst{\Ple}p do teorii liczb} (Eng. {\em Introduction to Number Theory}) by W. Sierpi\'nski, WSiP, Biblioteczka Matematyczna, Warszawa, 1987. The first few pages of this book have already been formalized in MML. We prove the Chinese Remainder Theorem and Thue's Theorem as well as several useful number theory propositions.

MML Identifier: WSIERP_1

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek. Joining of decorated trees. Journal of Formalized Mathematics, 5, 1993.

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.

[7] Katarzyna Jankowska. Transpose matrices and groups of permutations. Journal of Formalized Mathematics, 4, 1992.

[8] Andrzej Kondracki. Basic properties of rational numbers. Journal of Formalized Mathematics, 2, 1990.

[9] Jaroslaw Kotowicz and Yatsuka Nakamura. Introduction to Go-Board --- part I. Journal of Formalized Mathematics, 4, 1992.

[10] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[12] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[13] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[14] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[15] Wojciech A. Trybulec. Groups. Journal of Formalized Mathematics, 2, 1990.

[16] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[17] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.