Euler's totient function
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Gregor Perčič.
Created on 2022-03-09.
Last modified on 2023-11-24.
{-# OPTIONS --allow-unsolved-metas #-} module elementary-number-theory.eulers-totient-function where
Imports
open import elementary-number-theory.natural-numbers open import elementary-number-theory.relatively-prime-natural-numbers open import univalent-combinatorics.decidable-subtypes open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types
Idea
Euler's totient function φ : ℕ → ℕ is the function that maps a
natural number n to the number
of
multiplicative units modulo n.
In other words, the number φ n is the cardinality of the
group of units of the
ring ℤ-Mod n.
Alternatively, Euler's totient function can be defined as the function ℕ → ℕ
that returns for each n the number of x < n that are
relatively prime.
These two definitions of Euler's totient function agree on the positive
natural numbers. However, there are two multiplicative units in the
ring ℤ of
integers, while there are no natural
numbers x < 0 that are relatively prime to 0.
Our reason for preferring the first definition over the second definition is that the usual properties of Euler's totient function, such as multiplicativity, extend naturally to the first definition.
Definitions
The definition of Euler's totient function using relatively prime natural numbers
eulers-totient-function-relatively-prime : ℕ → ℕ eulers-totient-function-relatively-prime n = number-of-elements-subset-𝔽 ( Fin-𝔽 n) ( λ x → is-relatively-prime-ℕ-Decidable-Prop (nat-Fin n x) n)
See also
Table of files related to cyclic types, groups, and rings
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
- 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).