card_units_zmod_lt_sub_one — Mathlib

English

For p > 1, the unit group of ZMod p has at most p−1 elements: |(ZMod p)×| ≤ p−1.

Русский

Для p > 1 группа единиц ZMod p имеет не более p−1 элементов: |(ZMod p)×| ≤ p−1.

LaTeX

$$$$|\bigl(\mathbb{Z}/p\mathbb{Z}\bigr)^{\times}| \le p-1 \quad( p>1 ).$$$$

Lean4

theorem card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [Fintype (ZMod p)ˣ] : Fintype.card (ZMod p)ˣ ≤ p - 1 :=
  by
  haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩
  rw [ZMod.card_units_eq_totient p]
  exact Nat.le_sub_one_of_lt (Nat.totient_lt p hp)

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