pow_eq_one_iff_modEq

Mathlib.GroupTheory.OrderOfElement

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

English

For any x and n, x^n = 1 if and only if n is congruent to 0 modulo ord(x).

Русский

Для любых x и n, x^n = 1 тогда и только тогда, когда n ≡ 0 (mod ord(x)).

LaTeX

$$$ \forall G [Monoid G], \forall x : G, \forall n : \mathbb{N}, x^n = 1 \iff n \equiv 0 \pmod{ord(x)}$$$

Lean4

@[to_additive]
theorem pow_eq_one_iff_modEq : x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x] := by
  rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]

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

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

Разделы

Аффилиация

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