English
For n > 0, the number of units in ZMod n equals φ(n).
Русский
Для n > 0 число единиц в ZMod n равно φ(n).
LaTeX
$$$$| (\mathbb{Z}/n\mathbb{Z})^{\times} | = \varphi(n) \quad\text{when } n>0.$$$$
Lean4
/-- Note this takes an explicit `Fintype ((ZMod n)ˣ)` argument to avoid trouble with instance
diamonds. -/
@[simp]
theorem _root_.ZMod.card_units_eq_totient (n : ℕ) [NeZero n] [Fintype (ZMod n)ˣ] : Fintype.card (ZMod n)ˣ = φ n :=
calc
Fintype.card (ZMod n)ˣ = Fintype.card { x : ZMod n // x.val.Coprime n } := Fintype.card_congr ZMod.unitsEquivCoprime
_ = φ n := by
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ← Fin.sum_univ_eq_sum_range,
@Nat.coprime_comm (m + 1)]
rfl
