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.

def Nat.termφ : Lean.ParserDescr

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

@[simp]

theorem Nat.totient_zero : totient 0 = 0

@[simp]

theorem Nat.totient_one : totient 1 = 1

theorem Nat.totient_eq_card_coprime (n : ℕ) : n.totient = {a ∈ Finset.range n | n.Coprime a}.card

theorem Nat.totient_eq_card_lt_and_coprime (n : ℕ) : n.totient = Nat.card ↑{m : ℕ | m < n ∧ n.Coprime m}

A characterisation of Nat.totient that avoids Finset.

theorem Nat.totient_le (n : ℕ) : n.totient ≤ n

theorem Nat.totient_lt (n : ℕ) (hn : 1 < n) : n.totient < n

@[simp]

theorem Nat.totient_eq_zero {n : ℕ} : n.totient = 0 ↔ n = 0

@[simp]

theorem Nat.totient_pos {n : ℕ} : 0 < n.totient ↔ 0 < n

instance Nat.neZero_totient {n : ℕ} [NeZero n] : NeZero n.totient

theorem Nat.filter_coprime_Ico_eq_totient (a n : ℕ) : {x ∈ Finset.Ico n (n + a) | a.Coprime x}.card = a.totient

theorem Nat.Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_ne_zero : a ≠ 0) : {x ∈ Finset.Ico k (k + n) | a.Coprime x}.card ≤ a.totient * (n / a + 1)

@[simp]

theorem ZMod.card_units_eq_totient (n : ℕ) [NeZero 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) : Even n.totient

theorem Nat.totient_mul {m n : ℕ} (h : m.Coprime n) : (m * n).totient = m.totient * n.totient

theorem Nat.totient_div_of_dvd {n d : ℕ} (hnd : d ∣ n) : (n / d).totient = {k ∈ Finset.range n | n.gcd k = d}.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 : ℕ) : n.divisors.sum totient = n

theorem Nat.sum_totient' (n : ℕ) : ∑ m ∈ Finset.range n.succ with m ∣ n, m.totient = n

theorem Nat.totient_prime_pow_succ {p : ℕ} (hp : 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 : 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 : Prime p) : p.totient = p - 1

theorem Nat.totient_eq_iff_prime {p : ℕ} (hp : 0 < p) : p.totient = p - 1 ↔ 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)ˣ] : Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

@[simp]

theorem Nat.totient_two : totient 2 = 1

theorem Nat.odd_totient_iff {n : ℕ} : Odd n.totient ↔ n = 1 ∨ n = 2

Euler's totient function is only odd at 1 or 2.

theorem Nat.totient_eq_one_iff {n : ℕ} : n.totient = 1 ↔ n = 1 ∨ n = 2

theorem Nat.dvd_two_of_totient_le_one {a : ℕ} (han : 0 < a) (ha : a.totient ≤ 1) : a ∣ 2

theorem Nat.odd_totient_iff_eq_one {n : ℕ} : Odd n.totient ↔ n.totient = 1

theorem Nat.totient_coprime_totient_iff (m n : ℕ) : m.totient.Coprime n.totient ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Nat.totient m and Nat.totient n are coprime iff one of them is 1.

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 fun (p k : ℕ) => p ^ (k - 1) * (p - 1)

Euler's product formula for the totient function.

theorem Nat.totient_mul_prod_primeFactors (n : ℕ) : n.totient * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Euler's product formula for the totient function.

theorem Nat.totient_eq_div_primeFactors_mul (n : ℕ) : n.totient = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Euler's product formula for the totient function.

theorem Nat.totient_eq_mul_prod_factors (n : ℕ) : ↑n.totient = ↑n * ∏ p ∈ n.primeFactors, (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_super_multiplicative (a b : ℕ) : a.totient * b.totient ≤ (a * b).totient

theorem Nat.totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : a.totient ∣ b.totient

theorem Nat.totient_mul_of_prime_of_dvd {p n : ℕ} (hp : Prime p) (h : p ∣ n) : (p * n).totient = p * n.totient

theorem Nat.totient_mul_of_prime_of_not_dvd {p n : ℕ} (hp : Prime p) (h : ¬p ∣ n) : (p * n).totient = (p - 1) * n.totient

theorem Nat.totient_two_mul_of_even {n : ℕ} (hn : Even n) : (2 * n).totient = 2 * n.totient

theorem Nat.totient_two_mul_of_odd {n : ℕ} (hn : Odd n) : (2 * n).totient = n.totient

theorem Nat.eq_or_eq_of_totient_eq_totient {a b : ℕ} (h : a ∣ b) (h' : a.totient = b.totient) : a = b ∨ 2 * a = b

theorem Even.eq_of_totient_eq_totient {a b : ℕ} (h : a ∣ b) (ha : Even a) (h' : a.totient = b.totient) : a = b

theorem Nat.prime_pow_pow_totient_ediv_prod {p k : ℕ} (hp : Prime p) (hk : 0 < k) : (p ^ k) ^ (p ^ k).totient / ∏ q ∈ (p ^ k).primeFactors, q ^ ((p ^ k).totient / (q - 1)) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

theorem Nat.prod_primeFactors_pow_totient_ediv_dvd {n : ℕ} (hn : 0 < n) : ∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1)) ∣ n ^ n.totient

def Mathlib.Meta.Positivity.evalNatTotient : PositivityExt

Extension for Nat.totient.