English
For all a,b ∈ ℕ, φ(gcd(a,b)) · φ(a b) = φ(a) · φ(b) · gcd(a,b).
Русский
Для всех a,b ∈ ℕ: φ(gcd(a,b)) · φ(a b) = φ(a) · φ(b) · gcd(a,b).
LaTeX
$$$$ \\varphi(\\gcd(a,b)) \\cdot \\varphi(a b) = \\varphi(a) \\cdot \\varphi(b) \\cdot \\gcd(a,b). $$$$
Lean4
theorem totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b :=
by
have shuffle :
∀ a1 a2 b1 b2 c1 c2 : ℕ, b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2) :=
by
intro a1 a2 b1 b2 c1 c2 h1 h2
calc
a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
_ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
congr 1
exact div_mul_div_comm h1 h2
simp only [totient_eq_div_primeFactors_mul]
rw [shuffle, shuffle]
rotate_left
repeat' apply prod_primeFactors_dvd
simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]
rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)
