orderOf_eq_prime

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

If x^p = 1 and x ≠ 1, then orderOf(x) = p.

Русский

Если x^p = 1 и x ≠ 1, то orderOf(x) = p.

LaTeX

$$x^p = 1 ∧ x ≠ 1 ⇒ \operatorname{orderOf}(x) = p$$

Lean4

/-- The backward direction of `orderOf_eq_prime_iff`. -/
@[to_additive /-- The backward direction of `addOrderOf_eq_prime_iff`. -/
    ]
theorem orderOf_eq_prime (hg : x ^ p = 1) (hg1 : x ≠ 1) : orderOf x = p :=
  orderOf_eq_prime_iff.mpr ⟨hg, hg1⟩

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

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

Разделы

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

Аффилиация

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