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.

Equations
    Instances For

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

      Equations
        Instances For
          @[simp]
          @[simp]

          A characterisation of Nat.totient that avoids Finset.

          theorem Nat.totient_le (n : ) :
          theorem Nat.totient_lt (n : ) (hn : 1 < n) :
          @[simp]
          theorem Nat.totient_eq_zero {n : } :
          n.totient = 0 n = 0
          @[simp]
          theorem Nat.totient_pos {n : } :
          0 < n.totient 0 < n
          theorem Nat.filter_coprime_Ico_eq_totient (a n : ) :
          {xFinset.Ico n (n + a) | a.Coprime x}.card = a.totient
          theorem Nat.Ico_filter_coprime_le {a : } (k n : ) (a_pos : 0 < a) :
          {xFinset.Ico k (k + n) | a.Coprime x}.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 = {kFinset.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 : ) :
          mFinset.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
          @[simp]
          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

          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 * pn.primeFactors, p = n * pn.primeFactors, (p - 1)

          Euler's product formula for the totient function.

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

          Euler's product formula for the totient function.

          theorem Nat.totient_eq_mul_prod_factors (n : ) :
          n.totient = n * pn.primeFactors, (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 : 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