orderOf_units_dvd_card_sub_one — Mathlib

English

Let p be a prime and u a unit in Z/pZ. Then the multiplicative order of u divides p−1.

Русский

Пусть p — простое число и u — единичный элемент в Z/pZ. Тогда порядок умножения u делит p−1.

LaTeX

$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\Rightarrow \\\\forall u \\\\in (\\\\mathbb{Z}/p\\\\mathbb{Z})^{\\\\times}, \\\\operatorname{ord}(u) \\\\mid (p-1)$$$

Lean4

theorem orderOf_units_dvd_card_sub_one (u : (ZMod p)ˣ) : orderOf u ∣ p - 1 :=
  orderOf_dvd_of_pow_eq_one <| units_pow_card_sub_one_eq_one _ _

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