English
For d | n, φ(n/d) equals the number of k < n with gcd(n,k) = d.
Русский
Для d делится на n верно φ(n/d) = #{ k < n : gcd(n,k) = d }.
LaTeX
$$$$\varphi\left(\frac{n}{d}\right) = \#\{ k ∈ \{0,1,\dots, n-1\} : \gcd(n,k) = d \}, \quad d \mid n.$$$$
Lean4
theorem totient_mul {m n : ℕ} (h : m.Coprime n) : φ (m * n) = φ m * φ n :=
if hmn0 : m * n = 0 then by
rcases Nat.mul_eq_zero.1 hmn0 with h | h <;> simp only [totient_zero, mul_zero, zero_mul, h]
else by
haveI : NeZero (m * n) := ⟨hmn0⟩
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
simp only [← ZMod.card_units_eq_totient]
rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]
