Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

The Euler's Function


Yoshinori Fujisawa
Shinshu University, Nagano
Yasushi Fuwa
Shinshu University, Nagano

Summary.

This article is concerned with the Euler's function [10] that plays an important role in cryptograms. In the first section, we present some selected theorems on integers. Next, we define the Euler's function. Finally, three theorems relating to the Euler's function are proved. The third theorem concerns two relatively prime integers which make up the Euler's function parameter. In the public key cryptography these two integer values are used as public and secret keys.

MML Identifier: EULER_1

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

Contents (PDF format)

  1. Preliminary
  2. Euler's Function --- Definition and theorems

Acknowledgments

The authors wish to thank Professor A. Trybulec for all his advice on this article.

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. Sequences of ordinal numbers. 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] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[9] Rafal Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Journal of Formalized Mathematics, 2, 1990.
[10] Teiji Takagi. \em Elementary Theory of Numbers. Kyoritsu Publishing Co., Ltd., second edition, 1995.
[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] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[14] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[15] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received December 10, 1997

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