orderOf_le_exponent — Mathlib

English

Let G be a monoid with ExponentExists. Then for any g in G, the order of g is at most the exponent of G.

Русский

Пусть G — моноид с существованием экспоненты. Тогда для любого g ∈ G порядок элемента g не превосходит экспоненты G.

LaTeX

$$$(\\\\operatorname{orderOf} g) \\\\le \\\\operatorname{exponent} G$$$

Lean4

@[to_additive]
theorem orderOf_le_exponent (h : ExponentExists G) (g : G) : orderOf g ≤ exponent G :=
  Nat.le_of_dvd h.exponent_pos (order_dvd_exponent g)

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