orderOf_pos

Mathlib.GroupTheory.Exponent

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

English

If a type has a finite exponent, then every element has positive order.

Русский

Если существует экспонента, тогда для каждого элемента порядок положителен.

LaTeX

$$$\\forall g:G, 0 < \\operatorname{orderOf}(g)$$$

Lean4

@[to_additive]
theorem orderOf_pos (h : ExponentExists G) (g : G) : 0 < orderOf g :=
  h.isOfFinOrder.orderOf_pos

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

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

Разделы

Аффилиация

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