exponent_ne_zero_of_finite — Mathlib

English

If G is a finite, left-cancellative monoid, then there exists an exponent for G (i.e., an integer e such that g^e = 1 for all g in G).

Русский

Если G — конечный леволокальный моноид, то существует экспонента G (существует e, такое что для каждого g ∈ G выполняется g^e = 1).

LaTeX

$$$\\\\exists e \\\\in \\\\mathbb{N}, \\\\forall g : G, \\\\operatorname{pow}(g,e) = 1$$$

Lean4

@[to_additive]
theorem exponent_ne_zero_of_finite : exponent G ≠ 0 :=
  ExponentExists.of_finite.exponent_ne_zero

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