pow_ne_one_of_lt_orderOf

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

If 0 < n and x^n = 1, then orderOf x ≤ n.

Русский

Если 0 < n и x^n = 1, то orderOf x ≤ n.

LaTeX

$$0 < n \\Rightarrow (x^n = 1 \\Rightarrow orderOf x \\le n)$$

Lean4

@[to_additive]
theorem pow_ne_one_of_lt_orderOf (n0 : n ≠ 0) (h : n < orderOf x) : x ^ n ≠ 1 := fun j =>
  not_isPeriodicPt_of_pos_of_lt_minimalPeriod n0 h ((isPeriodicPt_mul_iff_pow_eq_one x).mpr j)

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

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

Разделы

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

Аффилиация

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