totient_dvd_of_dvd — Mathlib

English

If a divides b, then φ(a) divides φ(b).

Русский

Если a делит b, то φ(a) делит φ(b).

LaTeX

$$$$ a \\\\mid b \\\\Rightarrow \\\\varphi(a) \\\\mid \\\\varphi(b). $$$$

Lean4

@[gcongr]
theorem totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : φ a ∣ φ b :=
  by
  rcases eq_or_ne a 0 with (rfl | ha0)
  · simp [zero_dvd_iff.1 h]
  rcases eq_or_ne b 0 with (rfl | hb0)
  · simp
  have hab' := primeFactors_mono h hb0
  rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
  refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl
  exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)

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