orderOf_le_card_univ — Mathlib

English

Let G be a finite monoid. For every element x in G, the order of x is at most the cardinality of G.

Русский

Пусть G является конечным моноидом. Для каждого элемента x ∈ G порядок x не превосходит кардиналность G.

LaTeX

$$$\operatorname{orderOf}(x) \le \lvert G \rvert$$$

Lean4

@[to_additive]
theorem orderOf_le_card_univ [Fintype G] : orderOf x ≤ Fintype.card G :=
  Finset.le_card_of_inj_on_range (x ^ ·) (fun _ _ ↦ Finset.mem_univ _) pow_injOn_Iio_orderOf

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