orderOf_eq

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#Subsingleton.orderOf_eq

English

In a subsingleton monoid, every element has order 1.

Русский

В подмножестве единичного типа каждый элемент имеет порядок 1.

LaTeX

$$orderOf x = 1$$

Lean4

@[to_additive (attr := nontriviality)]
theorem orderOf_eq [Subsingleton G] (x : G) : orderOf x = 1 := by simp [orderOf, nontriviality]

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

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

Разделы

Аффилиация

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