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-09-21.

{-# 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 elementary-number-theory.sums-of-natural-numbers

open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types

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)

Recent changes