totient_prime

formal source

 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
 130  simp only [totient]
 131  exact Nat.totient_le n
 132
 133/-- φ(n) > 0 iff n > 0. -/
 134theorem totient_pos_iff {n : ℕ} : 0 < totient n ↔ 0 < n := by
 135  simp only [totient]
 136  exact Nat.totient_pos
 137
 138/-! ### Von Mangoldt function Λ -/