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
@[simp]
theorem nat.totient_zero  :
@[simp]
theorem nat.totient_one  :
theorem nat.totient_le (n : ) :
theorem nat.totient_pos {n : } :
0 < n0 < n.totient
@[simp]
theorem zmod.card_units_eq_totient (n : ) [fact (0 < 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 ^ 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) :
@[simp]
theorem nat.totient_two  :