zpow_eq_one_iff_modEq

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

For any x in a group, and integer n, x^n = 1 iff n ≡ 0 (mod orderOf x).

Русский

Для любого x в группе и целого n, x^n = 1 тогда и только тогда, когда n ≡ 0 (mod orderOf x).

LaTeX

$$x^n = 1 \iff n \equiv 0 \pmod{\operatorname{orderOf}(x)}$$

Lean4

@[to_additive]
theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by
  rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]

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

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

Разделы

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

Аффилиация

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