totient_super_multiplicative — Mathlib

English

For all a,b ∈ ℕ, φ(a) φ(b) ≤ φ(a b).

Русский

Для всех a,b ∈ ℕ: φ(a) φ(b) ≤ φ(a b).

LaTeX

$$$$ \\varphi(a) \\cdot \\varphi(b) \\le \\varphi(a b). $$$$

Lean4

theorem totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) :=
  by
  let d := a.gcd b
  rcases (zero_le a).eq_or_lt with (rfl | ha0)
  · simp
  have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
  apply le_of_mul_le_mul_right _ hd0
  rw [← totient_gcd_mul_totient_mul a b, mul_comm]
  apply mul_le_mul_left' (Nat.totient_le d)

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