English
For all n, φ(n) equals the cardinality of the set {m | m < n and gcd(n,m) = 1}.
Русский
Для любого n φ(n) равно кардинальности множества {m | m < n и gcd(n,m) = 1}.
LaTeX
$$$$\varphi(n) = \#\{m ∈ \mathbb{N} : m < n \wedge \gcd(n,m)=1\}.$$$$
Lean4
/-- A characterisation of `Nat.totient` that avoids `Finset`. -/
theorem totient_eq_card_lt_and_coprime (n : ℕ) : φ n = Nat.card {m | m < n ∧ n.Coprime m} :=
by
let e : {m | m < n ∧ n.Coprime m} ≃ {x ∈ range n | n.Coprime x} :=
{ toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
left_inv := fun m => by simp only [Subtype.coe_eta]
right_inv := fun m => by simp only [Subtype.coe_eta] }
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
