totient_prime_pow — Mathlib

English

If p is prime and n ≥ 1, φ(p^n) = p^{n-1}(p-1).

Русский

Если p простое и n ≥ 1, φ(p^n) = p^{n-1}(p-1).

LaTeX

$$$$\varphi(p^{n}) = p^{n-1}(p-1)\qquad(\text{поскольку } n>0).$$$$

Lean4

/-- When `p` is prime, then the totient of `p ^ n` is `p ^ (n - 1) * (p - 1)` -/
theorem 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 _

Похожие утверждения