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

• Nat.totient n = (Finset.filter (Nat.Coprime n) (Finset.range n)).card

def Nat.termφ : Lean.ParserDescr

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

Equations

• Nat.termφ = Lean.ParserDescr.node `Nat.termφ 1024 (Lean.ParserDescr.symbol "φ")

@[simp]

theorem Nat.totient_zero : Nat.totient 0 = 0

@[simp]

theorem Nat.totient_one : Nat.totient 1 = 1

theorem Nat.totient_eq_card_coprime (n : ℕ) : Nat.totient n = (Finset.filter (Nat.Coprime n) (Finset.range n)).card

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

A characterisation of Nat.totient that avoids Finset.

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

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

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

theorem Nat.filter_coprime_Ico_eq_totient (a : ℕ) (n : ℕ) : (Finset.filter (Nat.Coprime a) (Finset.Ico n (n + a))).card = Nat.totient a

theorem Nat.Ico_filter_coprime_le {a : ℕ} (k : ℕ) (n : ℕ) (a_pos : 0 < a) : (Finset.filter (Nat.Coprime a) (Finset.Ico k (k + n))).card ≤ Nat.totient a * (n / a + 1)

@[simp]

theorem ZMod.card_units_eq_totient (n : ℕ) [NeZero n] [Fintype (ZMod n)ˣ] : Fintype.card (ZMod n)ˣ = Nat.totient 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 (Nat.totient n)

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

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

theorem Nat.sum_totient' (n : ℕ) : (Finset.sum (Finset.filter (fun (x : ℕ) => x ∣ n) (Finset.range (Nat.succ n))) fun (m : ℕ) => Nat.totient m) = n

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

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

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

theorem Nat.dvd_two_of_totient_le_one {a : ℕ} (han : 0 < a) (ha : Nat.totient a ≤ 1) : a ∣ 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) : Nat.totient n = Finsupp.prod (Nat.factorization n) fun (p k : ℕ) => p ^ (k - 1) * (p - 1)

Euler's product formula for the totient function.

theorem Nat.totient_mul_prod_primeFactors (n : ℕ) : (Nat.totient n * Finset.prod n.primeFactors fun (p : ℕ) => p) = n * Finset.prod n.primeFactors fun (p : ℕ) => p - 1

Euler's product formula for the totient function.

theorem Nat.totient_eq_div_primeFactors_mul (n : ℕ) : Nat.totient n = (n / Finset.prod n.primeFactors fun (p : ℕ) => p) * Finset.prod n.primeFactors fun (p : ℕ) => p - 1

Euler's product formula for the totient function.

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

Euler's product formula for the totient function.

theorem Nat.totient_gcd_mul_totient_mul (a : ℕ) (b : ℕ) : Nat.totient (Nat.gcd a b) * Nat.totient (a * b) = Nat.totient a * Nat.totient b * Nat.gcd a b

theorem Nat.totient_super_multiplicative (a : ℕ) (b : ℕ) : Nat.totient a * Nat.totient b ≤ Nat.totient (a * b)

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

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

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