mathlib3 documentation

data.nat.totient

Euler's totient function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Equations
@[simp]
theorem nat.totient_zero  :
@[simp]
theorem nat.totient_one  :

A characterisation of nat.totient that avoids finset.

theorem nat.totient_le (n : ) :
theorem nat.totient_lt (n : ) (hn : 1 < n) :
theorem nat.totient_pos {n : } :
0 < n 0 < n.totient
theorem nat.Ico_filter_coprime_le {a : } (k n : ) (a_pos : 0 < a) :
(finset.filter a.coprime (finset.Ico k (k + n))).card a.totient * (n / a + 1)
@[simp]

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

theorem nat.totient_even {n : } (hn : 2 < n) :
theorem nat.totient_mul {m n : } (h : m.coprime n) :
theorem nat.totient_div_of_dvd {n d : } (hnd : d n) :
(n / d).totient = (finset.filter (λ (k : ), n.gcd k = d) (finset.range n)).card

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 : ) :
(finset.filter (λ (_x : ), _x n) (finset.range n.succ)).sum (λ (m : ), m.totient) = n
theorem nat.totient_prime_pow_succ {p : } (hp : nat.prime p) (n : ) :
(p ^ (n + 1)).totient = 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 : nat.prime p) {n : } (hn : 0 < n) :
(p ^ n).totient = 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 : nat.prime p) :
p.totient = p - 1
theorem nat.totient_eq_iff_prime {p : } (hp : 0 < p) :
theorem nat.card_units_zmod_lt_sub_one {p : } (hp : 1 < p) [fintype (zmod p)ˣ] :
@[simp]
theorem nat.totient_two  :
theorem nat.totient_eq_one_iff {n : } :
n.totient = 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) :
n.totient = n.factorization.prod (λ (p k : ), p ^ (k - 1) * (p - 1))

Euler's product formula for the totient function.

theorem nat.totient_mul_prod_factors (n : ) :
n.totient * n.factors.to_finset.prod (λ (p : ), p) = n * n.factors.to_finset.prod (λ (p : ), p - 1)

Euler's product formula for the totient function.

theorem nat.totient_eq_div_factors_mul (n : ) :
n.totient = n / n.factors.to_finset.prod (λ (p : ), p) * n.factors.to_finset.prod (λ (p : ), p - 1)

Euler's product formula for the totient function.

theorem nat.totient_eq_mul_prod_factors (n : ) :
(n.totient) = n * n.factors.to_finset.prod (λ (p : ), 1 - (p)⁻¹)

Euler's product formula for the totient function.

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