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]

Preliminary

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]