# Documentation

Mathlib.Data.Nat.Totient

# Euler's totient function #

This file defines Euler's totient function Nat.totient n which counts the number of naturals less than n that are coprime with n. We prove the divisor sum formula, namely that n equals φ summed over the divisors of n. See sum_totient. We also prove two lemmas to help compute totients, namely totient_mul and totient_prime_pow.

def Nat.totient (n : ) :

Euler's totient function. This counts the number of naturals strictly less than n which are coprime with n.

Instances For

Euler's totient function. This counts the number of naturals strictly less than n which are coprime with n.

Instances For
@[simp]
theorem Nat.totient_zero :
= 0
@[simp]
theorem Nat.totient_one :
= 1
theorem Nat.totient_eq_card_lt_and_coprime (n : ) :
= Nat.card {m | m < n }

A characterisation of Nat.totient that avoids Finset.

theorem Nat.totient_le (n : ) :
n
theorem Nat.totient_lt (n : ) (hn : 1 < n) :
< n
theorem Nat.totient_pos {n : } :
0 < n0 <
theorem Nat.Ico_filter_coprime_le {a : } (k : ) (n : ) (a_pos : 0 < a) :
Finset.card (Finset.filter () (Finset.Ico k (k + n))) * (n / a + 1)
@[simp]
theorem ZMod.card_units_eq_totient (n : ) [] [Fintype (ZMod n)ˣ] :

Note this takes an explicit Fintype ((ZMod n)ˣ) argument to avoid trouble with instance diamonds.

theorem Nat.totient_even {n : } (hn : 2 < n) :
Even ()
theorem Nat.totient_mul {m : } {n : } (h : ) :
Nat.totient (m * n) =
theorem Nat.totient_div_of_dvd {n : } {d : } (hnd : d n) :
Nat.totient (n / d) = Finset.card (Finset.filter (fun k => Nat.gcd n k = d) ())

For d ∣ n, the totient of n/d equals the number of values k < n such that gcd n k = d

theorem Nat.sum_totient (n : ) :
theorem Nat.sum_totient' (n : ) :
(Finset.sum (Finset.filter (fun x => x n) ()) fun m => ) = n
theorem Nat.totient_prime_pow_succ {p : } (hp : ) (n : ) :
Nat.totient (p ^ (n + 1)) = p ^ n * (p - 1)

When p is prime, then the totient of p ^ (n + 1) is p ^ n * (p - 1)

theorem Nat.totient_prime_pow {p : } (hp : ) {n : } (hn : 0 < n) :
Nat.totient (p ^ n) = p ^ (n - 1) * (p - 1)

When p is prime, then the totient of p ^ n is p ^ (n - 1) * (p - 1)

theorem Nat.totient_prime {p : } (hp : ) :
= p - 1
theorem Nat.totient_eq_iff_prime {p : } (hp : 0 < p) :
= p - 1
theorem Nat.card_units_zmod_lt_sub_one {p : } (hp : 1 < p) [Fintype (ZMod p)ˣ] :
p - 1
@[simp]
theorem Nat.totient_two :
= 1
theorem Nat.totient_eq_one_iff {n : } :
= 1 n = 1 n = 2

### Euler's product formula for the totient function #

We prove several different statements of this formula.

theorem Nat.totient_eq_prod_factorization {n : } (hn : n 0) :
= Finsupp.prod () fun p k => p ^ (k - 1) * (p - 1)

Euler's product formula for the totient function.

theorem Nat.totient_mul_prod_factors (n : ) :
( * Finset.prod () fun p => p) = n * Finset.prod () fun p => p - 1

Euler's product formula for the totient function.

theorem Nat.totient_eq_div_factors_mul (n : ) :
= (n / Finset.prod () fun p => p) * Finset.prod () fun p => p - 1

Euler's product formula for the totient function.

theorem Nat.totient_eq_mul_prod_factors (n : ) :
↑() = n * Finset.prod () fun p => 1 - (p)⁻¹

Euler's product formula for the totient function.

theorem Nat.totient_dvd_of_dvd {a : } {b : } (h : a b) :
theorem Nat.totient_mul_of_prime_of_dvd {p : } {n : } (hp : ) (h : p n) :
Nat.totient (p * n) = p *
theorem Nat.totient_mul_of_prime_of_not_dvd {p : } {n : } (hp : ) (h : ¬p n) :
Nat.totient (p * n) = (p - 1) *