English
For p, prime ↔ Fintype.card(ZMod p)× = p−1.
Русский
Для p простое тогда и только тогда, когда |(ZMod p)×| = p−1.
LaTeX
$$$$p \text{ prime} \iff |(\mathbb{Z}/p\mathbb{Z})^{\times}| = p-1.$$$$
Lean4
theorem prime_iff_card_units (p : ℕ) [Fintype (ZMod p)ˣ] : p.Prime ↔ Fintype.card (ZMod p)ˣ = p - 1 :=
by
rcases eq_zero_or_neZero p with hp | hp
· subst hp
simp only [ZMod, not_prime_zero, false_iff, zero_tsub]
-- the subst created a non-defeq but subsingleton instance diamond; resolve it
suffices Fintype.card ℤˣ ≠ 0 by convert this
simp
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]