exponent — Mathlib

English

From ExponentExists, every element has finite order: IsOfFinOrder g for all g.

Русский

Из существования экспоненты следует, что каждый элемент имеет конечный порядок: IsOfFinOrder g для всех g.

LaTeX

$$$\\forall g:G, \\exists n>0\\, g^n=1$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.MulOpposite.exponent : exponent (MulOpposite G) = exponent G :=
  by
  simp only [Monoid.exponent, ExponentExists]
  congr!
  all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

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