# 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.

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)


ConceptFile
Acyclic mapssynthetic-homotopy-theory.acyclic-maps
Acyclic typessynthetic-homotopy-theory.acyclic-types
Acyclic undirected graphsgraph-theory.acyclic-undirected-graphs
Braceletsunivalent-combinatorics.bracelets
The category of cyclic ringsring-theory.category-of-cyclic-rings
The circlesynthetic-homotopy-theory.circle
Connected set bundles over the circlesynthetic-homotopy-theory.connected-set-bundles-circle
Cyclic finite typesunivalent-combinatorics.cyclic-finite-types
Cyclic groupsgroup-theory.cyclic-groups
Cyclic higher groupshigher-group-theory.cyclic-higher-groups
Cyclic ringsring-theory.cyclic-rings
Cyclic typesstructured-types.cyclic-types
Euler's totient functionelementary-number-theory.eulers-totient-function
Finitely cyclic mapselementary-number-theory.finitely-cyclic-maps
Generating elements of groupsgroup-theory.generating-elements-groups
Hatcher's acyclic typesynthetic-homotopy-theory.hatchers-acyclic-type
Homomorphisms of cyclic ringsring-theory.homomorphisms-cyclic-rings
Infinite cyclic typessynthetic-homotopy-theory.infinite-cyclic-types
Multiplicative units in the standard cyclic ringselementary-number-theory.multiplicative-units-standard-cyclic-rings
Necklacesunivalent-combinatorics.necklaces
Polygonsgraph-theory.polygons
The poset of cyclic ringsring-theory.poset-of-cyclic-rings
Standard cyclic groups (ℤ/k)elementary-number-theory.standard-cyclic-groups
Standard cyclic rings (ℤ/k)elementary-number-theory.standard-cyclic-rings