Euler_Phi_Function_of_Prime_Power
Provedeuler-phi-functionprime-numbersproofwiki
φ(p^n) = (p-1) * p^(n-1) for prime p.
Preamble
import Mathlib.Data.Nat.Totient
Formal statement
theorem Euler_Phi_Function_of_Prime_Power (p : ℕ) (hp : Nat.Prime p) (n : ℕ) (hn : 0 < n) : Nat.totient (p ^ n) = (p - 1) * p ^ (n - 1) := by sorry
Source