Euler’s totient function
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Fernando Chu and Gregor Perčič.
Created on 2022-03-09.
Last modified on 2025-02-11.
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-Finite-Type ( Fin-Finite-Type n) ( λ x → is-relatively-prime-ℕ-Decidable-Prop (nat-Fin n x) n)
See also
Table of files related to cyclic types, groups, and rings
External links
- Euler’s totient function at Wikidata
- Euler’s totient function at Wikipedia
- Totient Function at Wolfram MathWorld
Recent changes
- 2025-02-11. Fredrik Bakke. Switch from
𝔽toFinite-*(#1312). - 2024-10-16. Fredrik Bakke. Some links in elementary number theory (#1199).
- 2024-08-29. Fernando Chu, Fredrik Bakke and Egbert Rijke. Cones, limits and reduced coslices of precats (#1161).
- 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).