`totient`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 99 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 99.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  96/-! ### Euler's totient function φ (via `Nat.totient`) -/
  97
  98/-- Euler's totient function wrapper. -/
  99def totient (n : ℕ) : ℕ := Nat.totient n
 100
 101@[simp] theorem totient_apply {n : ℕ} : totient n = Nat.totient n := rfl
 102
 103/-- φ(1) = 1. -/
 104theorem totient_one : totient 1 = 1 := by
 105  simp [totient, Nat.totient_one]
 106
 107/-- φ(p) = p - 1 for prime p. -/
 108theorem totient_prime {p : ℕ} (hp : Prime p) : totient p = p - 1 := by
 109  have hp' : Nat.Prime p := (prime_iff p).1 hp
 110  simp [totient, Nat.totient_prime hp']
 111
 112/-- φ(p^k) = p^(k-1) * (p - 1) for prime p and k ≥ 1. -/
 113theorem totient_prime_pow {p k : ℕ} (hp : Prime p) (hk : 0 < k) :
 114    totient (p ^ k) = p ^ (k - 1) * (p - 1) := by
 115  have hp' : Nat.Prime p := (prime_iff p).1 hp
 116  simp [totient, Nat.totient_prime_pow hp' hk]
 117
 118/-- φ is multiplicative for coprime arguments. -/
 119theorem totient_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
 120    totient (m * n) = totient m * totient n := by
 121  simp [totient, Nat.totient_mul h]
 122
 123/-- The sum of φ(d) over divisors of n equals n: ∑_{d|n} φ(d) = n. -/
 124theorem totient_divisor_sum {n : ℕ} : ∑ d ∈ n.divisors, totient d = n := by
 125  simp only [totient]
 126  exact Nat.sum_totient n
 127
 128/-- φ(n) ≤ n for all n. -/
 129theorem totient_le (n : ℕ) : totient n ≤ n := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.