Prime powers with totient one

Mathlib's Nat.totient_eq_one_iff says that φ(n) = 1 exactly for n = 1 and n = 2. This file specialises it to prime powers: φ(p ^ k) = 1 exactly when k = 0, or p = 2 and k = 1.

Main results

• TauCeti.Nat.totient_prime_pow_eq_one_iff: for a prime p, φ(p ^ k) = 1 iff k = 0, or p = 2 and k = 1.

theorem TauCeti.Nat.totient_prime_pow_eq_one_iff {p k : ℕ} (hp : Nat.Prime p) : (p ^ k).totient = 1 ↔ k = 0 ∨ p = 2 ∧ k = 1

For a prime p, the totient of p ^ k is one exactly when k = 0, or p = 2 and k = 1.