case intro
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < succ m
⊢ φ (p ^ succ m) = p ^ (succ m - 1) * (p - 1)
p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)
rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩
no goals
case intro
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < succ m
⊢ φ (p ^ succ m) = p ^ (succ m - 1) * (p - 1)
exact totient_prime_pow_succ hp _