order_dvd_exponent — Mathlib

English

Let G be a monoid. Then for every element g in G, the order of g divides the exponent of G.

Русский

Пусть G — моноид. Тогда для каждого элемента g ∈ G выполняется, что порядок элемента g делит экспоненту G.

LaTeX

$$$\\\\forall g : G, \\\\operatorname{orderOf} g \\\\mid \\\\operatorname{exponent} G$$$

Lean4

@[to_additive addOrder_dvd_exponent]
theorem order_dvd_exponent (g : G) : orderOf g ∣ exponent G :=
  orderOf_dvd_of_pow_eq_one <| pow_exponent_eq_one g

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