feat(data/nat/totient): totient_prime_pow (#8353)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Author: ChrisHughes24

src/data/nat/gcd.lean

@@ -342,6 +342,18 @@ theorem coprime.pow_right {m k : ℕ} (n : ℕ) (H1 : coprime k m) : coprime k (
 theorem coprime.pow {k l : ℕ} (m n : ℕ) (H1 : coprime k l) : coprime (k ^ m) (l ^ n) :=
 (H1.pow_left _).pow_right _
 
+lemma coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ)  :
+  nat.coprime (a ^ n) b ↔ nat.coprime a b :=
+begin
+  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn.ne',
+  rw [pow_succ, nat.coprime_mul_iff_left],
+  exact ⟨and.left, λ hab, ⟨hab, hab.pow_left _⟩⟩
+end
+
+lemma coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ)  :
+  nat.coprime a (b ^ n) ↔ nat.coprime a b :=
+by rw [nat.coprime_comm, coprime_pow_left_iff hn, nat.coprime_comm]
+
 theorem coprime.eq_one_of_dvd {k m : ℕ} (H : coprime k m) (d : k ∣ m) : k = 1 :=
 by rw [← H.gcd_eq_one, gcd_eq_left d]
 

src/data/nat/totient.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import algebra.big_operators.basic
+import data.nat.prime
 import data.zmod.basic
 
 /-!
@@ -12,7 +13,8 @@ import data.zmod.basic
 This file defines [Euler's totient function][https://en.wikipedia.org/wiki/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`.
+`sum_totient`. We also prove two lemmas to help compute totients, namely `totient_mul` and
+`totient_prime_pow`.
 -/
 
 open finset
@@ -28,6 +30,11 @@ localized "notation `φ` := nat.totient" in nat
 
 @[simp] theorem totient_zero : φ 0 = 0 := rfl
 
+@[simp] theorem totient_one : φ 1 = 1 :=
+by simp [totient]
+
+lemma totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter (nat.coprime n)).card := rfl
+
 lemma totient_le (n : ℕ) : φ n ≤ n :=
 calc totient n ≤ (range n).card : card_filter_le _ _
            ... = n              : card_range _
@@ -120,4 +127,52 @@ calc ∑ m in (range n.succ).filter (∣ n), φ m
           (gcd_dvd_left _ _))), gcd_dvd_left _ _⟩, mem_filter.2 ⟨hm, rfl⟩⟩⟩))
 ... = n : card_range _
 
+/-- When `p` is prime, then the totient of `p ^ (n + 1)` is `p ^ n * (p - 1)` -/
+lemma totient_prime_pow_succ {p : ℕ} (hp : p.prime) (n : ℕ) :
+  φ (p ^ (n + 1)) = p ^ n * (p - 1) :=
+calc φ (p ^ (n + 1))
+    = ((range (p ^ (n + 1))).filter (coprime (p ^ (n + 1)))).card :
+  totient_eq_card_coprime _
+... = (range (p ^ (n + 1)) \ ((range (p ^ n)).image (* p))).card :
+  congr_arg card begin
+    rw [sdiff_eq_filter],
+    apply filter_congr,
+    simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos,
+      mem_image, not_exists, hp.coprime_iff_not_dvd],
+    intros a ha,
+    split,
+    { rintros hap b _ rfl,
+      exact hap (dvd_mul_left _ _) },
+    { rintros h ⟨b, rfl⟩,
+      rw [pow_succ] at ha,
+      exact h b (lt_of_mul_lt_mul_left ha (zero_le _)) (mul_comm _ _) }
+  end
+... = _ :
+have h1 : set.inj_on (* p) (range (p ^ n)),
+  from λ x _ y _, (nat.mul_left_inj hp.pos).1,
+have h2 : (range (p ^ n)).image (* p) ⊆ range (p ^ (n + 1)),
+  from λ a, begin
+    simp only [mem_image, mem_range, exists_imp_distrib],
+    rintros b h rfl,
+    rw [pow_succ'],
+    exact (mul_lt_mul_right hp.pos).2 h
+  end,
+begin
+  rw [card_sdiff h2, card_image_of_inj_on h1, card_range,
+    card_range, ← one_mul (p ^ n), pow_succ, ← nat.mul_sub_right_distrib,
+    one_mul, mul_comm]
+end
+
+/-- When `p` is prime, then the totient of `p ^ ` is `p ^ (n - 1) * (p - 1)` -/
+lemma totient_prime_pow {p : ℕ} (hp : p.prime) {n : ℕ} (hn : 0 < n) :
+  φ (p ^ n) = p ^ (n - 1) * (p - 1) :=
+by rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩;
+  exact totient_prime_pow_succ hp _
+
+lemma totient_prime {p : ℕ} (hp : p.prime) : φ p = p - 1 :=
+by rw [← pow_one p, totient_prime_pow hp]; simp
+
+@[simp] lemma totient_two : φ 2 = 1 :=
+(totient_prime prime_two).trans (by norm_num)
+
 end nat