orderOf_dvd_card_sub_one — Mathlib

English

If a is a nonzero element of Z/pZ, then the multiplicative order of a divides p−1.

Русский

Если a не равен нулю в Z/pZ, то порядок умножения a делит p−1.

LaTeX

$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\Rightarrow \\\\forall a \\\\in Z/pZ, \\\\text{a} \\\\neq 0 \\\\Rightarrow \\\\operatorname{ord}(a) \\\\mid (p-1)$$$

Lean4

theorem orderOf_dvd_card_sub_one {a : ZMod p} (ha : a ≠ 0) : orderOf a ∣ p - 1 :=
  orderOf_dvd_of_pow_eq_one <| pow_card_sub_one_eq_one ha

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