totient_mul_of_prime_of_not_dvd — Mathlib

English

If p is prime and p does not divide n, then φ(p n) = (p − 1) φ(n).

Русский

Если p — простое и p не делит n, то φ(p n) = (p − 1) φ(n).

LaTeX

$$$$ \\text{forall } p,n, \\\\text{ if } p \\\\text{ prime and } \\\\neg (p \\\\mid n), \\\\varphi(p n) = (p-1) \\\\cdot \\\\varphi(n). $$$$

Lean4

theorem totient_mul_of_prime_of_not_dvd {p n : ℕ} (hp : p.Prime) (h : ¬p ∣ n) : (p * n).totient = (p - 1) * n.totient :=
  by
  rw [totient_mul _, totient_prime hp]
  simpa [h] using coprime_or_dvd_of_prime hp n

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