prime_iff_card_units — Mathlib

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]

Похожие утверждения