isOfFinOrder

Mathlib.GroupTheory.Exponent

URI: https://scilib.ai/kg/mathlib#Monoid.ExponentExists.isOfFinOrder

English

If there exists a global exponent, then each g has finite order.

Русский

Если существует глобальная экспонента, то для каждого элемента g конечный порядок.

LaTeX

$$$\\forall g:G, \\text{IsOfFinOrder}(g)$$$

Lean4

@[to_additive]
theorem isOfFinOrder (h : ExponentExists G) {g : G} : IsOfFinOrder g :=
  isOfFinOrder_iff_pow_eq_one.mpr <| by peel 2 h; exact this g

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru