totient_mul_of_prime_of_dvd — Mathlib

English

If p is prime and p divides n, then φ(p n) = φ(p) φ(n).

Русский

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

LaTeX

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

Lean4

theorem totient_mul_of_prime_of_dvd {p n : ℕ} (hp : p.Prime) (h : p ∣ n) : (p * n).totient = p * n.totient :=
  by
  have h1 := totient_gcd_mul_totient_mul p n
  rw [gcd_eq_left h, mul_assoc] at h1
  simpa [(totient_pos.2 hp.pos).ne', mul_comm] using h1

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