isOfFinOrder_of_finite

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#isOfFinOrder_of_finite

English

If G is a finite left-cancellative monoid, every element has finite order.

Русский

Если G — конечный левонаCancellation моноид, у каждого элемента конечный порядок.

LaTeX

$$$\forall x \in G, \operatorname{IsOfFinOrder}(x)$$$

Lean4

@[to_additive]
theorem isOfFinOrder_of_finite (x : G) : IsOfFinOrder x := by by_contra h;
  exact infinite_not_isOfFinOrder h <| Set.toFinite _

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

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

Разделы

Аффилиация

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