English
If p is prime, then φ(p^(n+1)) = p^n (p-1).
Русский
Если p простое, то φ(p^{n+1}) = p^n (p-1).
LaTeX
$$$$\varphi(p^{n+1}) = p^{n}\,(p-1).$$$$
Lean4
/-- When `p` is prime, then the totient of `p ^ (n + 1)` is `p ^ n * (p - 1)` -/
theorem totient_prime_pow_succ {p : ℕ} (hp : p.Prime) (n : ℕ) : φ (p ^ (n + 1)) = p ^ n * (p - 1) :=
calc
φ (p ^ (n + 1)) = #({a ∈ range (p ^ (n + 1)) | (p ^ (n + 1)).Coprime a}) := totient_eq_card_coprime _
_ = #(range (p ^ (n + 1)) \ (range (p ^ n)).image (· * p)) :=
(congr_arg card
(by
rw [sdiff_eq_filter]
apply filter_congr
simp only [mem_range, coprime_pow_left_iff n.succ_pos, mem_image, not_exists, hp.coprime_iff_not_dvd]
intro a ha
constructor
· intro hap b h; rcases h with ⟨_, rfl⟩
exact hap (dvd_mul_left _ _)
· rintro h ⟨b, rfl⟩
rw [pow_succ'] at ha
exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩))
_ = _ := by
have h1 : Function.Injective (· * p) := mul_left_injective₀ hp.ne_zero
have h2 : (range (p ^ n)).image (· * p) ⊆ range (p ^ (n + 1)) := fun a =>
by
simp only [mem_image, mem_range, exists_imp]
rintro b ⟨h, rfl⟩
rw [Nat.pow_succ]
exact (mul_lt_mul_iff_left₀ hp.pos).2 h
rw [card_sdiff_of_subset h2, Finset.card_image_of_injective _ h1, card_range, card_range, ← one_mul (p ^ n),
pow_succ', ← tsub_mul, one_mul, mul_comm]
