orderOf_lt_card — Mathlib

English

In a finite monoid with zero, the order of any element is strictly less than the size of the monoid.

Русский

В конечном моноиде с нулём порядок любого элемента меньше размера моноида.

LaTeX

$$$\operatorname{orderOf}(a) < |M_0|$ for any $a \in M_0$$$

Lean4

theorem orderOf_lt_card [Finite M₀] (a : M₀) : orderOf a < Nat.card M₀ :=
  by
  by_cases h : IsUnit a
  · rw [← h.unit_spec, orderOf_units]
    exact orderOf_le_card.trans_lt <| natCard_units_lt M₀
  · rw [orderOf_eq_zero_iff'.mpr fun n hn ha ↦ h <| IsUnit.of_pow_eq_one ha hn.ne']
    exact Nat.card_pos

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