orderOf_lt — Mathlib

English

For ZMod n with n > 1, the order of any element is less than n.

Русский

Для кольца ZMod n с n > 1 порядок любого элемента меньше n.

LaTeX

$$$\forall a \in \mathbb{Z}/n\mathbb{Z}, \operatorname{order}(a) < n$ when $1 < n$$$

Lean4

theorem orderOf_lt {n : ℕ} (hn : 1 < n) (a : ZMod n) : orderOf a < n :=
  have : NeZero n := ⟨Nat.ne_zero_of_lt hn⟩
  have : Nontrivial (ZMod n) := nontrivial_iff.mpr hn.ne'
  (orderOf_lt_card a).trans_eq <| Nat.card_zmod n

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