orderOf_le_of_pow_eq_one

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

0 < n and x^n = 1 imply orderOf x ≤ n (variant).

Русский

0 < n и x^n = 1 влекут orderOf x ≤ n (вариант).

LaTeX

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

Lean4

@[to_additive]
theorem orderOf_le_of_pow_eq_one (hn : 0 < n) (h : x ^ n = 1) : orderOf x ≤ n :=
  IsPeriodicPt.minimalPeriod_le hn (by rwa [isPeriodicPt_mul_iff_pow_eq_one])

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

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

Разделы

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

Аффилиация

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