pow_orderOf_eq_one

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

If x has finite order, then 0 < orderOf x.

Русский

Если x имеет конечный порядок, тогда 0 < orderOf x.

LaTeX

$$IsOfFinOrder x \\Rightarrow 0 < orderOf x$$

Lean4

@[to_additive (attr := simp) addOrderOf_nsmul_eq_zero]
theorem pow_orderOf_eq_one (x : G) : x ^ orderOf x = 1 :=
  by
  convert Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)
  rw [orderOf, mul_left_iterate_apply_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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