mathlib documentation

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.

Equations

n.totient = (finset.filter n.coprime (finset.range n)).card

@[simp]

theorem nat.totient_zero :

@[simp]

theorem nat.totient_one :

theorem nat.totient_eq_card_coprime (n : ℕ) :

n.totient = (finset.filter n.coprime (finset.range n)).card

theorem nat.totient_le (n : ℕ) :

n.totient ≤ n

theorem nat.totient_lt (n : ℕ) (hn : 1 < n) :

theorem nat.totient_pos {n : ℕ} :

0 < n → 0 < n.totient

theorem nat.filter_coprime_Ico_eq_totient (a n : ℕ) :

(finset.filter a.coprime (finset.Ico n (n + a))).card = a.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]

theorem zmod.card_units_eq_totient (n : ℕ) [fact (0 < n)] [fintype (zmod n)ˣ] :

fintype.card (zmod n)ˣ = n.totient

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) :

(m * n).totient = (m.totient) * n.totient

theorem nat.sum_totient (n : ℕ) :

∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), 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_mul_of_prime_of_dvd {p n : ℕ} (hp : nat.prime p) (h : p ∣ n) :

(p * n).totient = p * n.totient

theorem nat.totient_eq_iff_prime {p : ℕ} (hp : 0 < p) :

p.totient = p - 1 ↔ nat.prime p

theorem nat.card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [fintype (zmod p)ˣ] :

fintype.card (zmod p)ˣ ≤ p - 1

theorem nat.prime_iff_card_units (p : ℕ) [fintype (zmod p)ˣ] :

nat.prime p ↔ fintype.card (zmod p)ˣ = p - 1

@[simp]

theorem nat.totient_two :

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) * ∏ (p : ℕ) in n.factors.to_finset, p = n * ∏ (p : ℕ) in n.factors.to_finset, (p - 1)

Euler's product formula for the totient function.

theorem nat.totient_eq_div_factors_mul (n : ℕ) :

n.totient = (n / ∏ (p : ℕ) in n.factors.to_finset, p) * ∏ (p : ℕ) in n.factors.to_finset, (p - 1)

Euler's product formula for the totient function.

theorem nat.totient_eq_mul_prod_factors (n : ℕ) :

↑(n.totient) = (↑n) * ∏ (p : ℕ) in n.factors.to_finset, (1 - (↑p)⁻¹)

Euler's product formula for the totient function.