orderOf_dvd_iff_zpow_eq_one — Mathlib

English

For any element x in a group, the integer (order of x) divides i if and only if x^i = 1.

Русский

Для любого элемента x в группе целое число order(x) делит i тогда и только тогда, когда x^i = 1.

LaTeX

$$$(\\operatorname{orderOf} x):\\mathbb{Z}$ divides i ⇔ x^i = 1$$

Lean4

@[to_additive]
theorem orderOf_dvd_iff_zpow_eq_one : (orderOf x : ℤ) ∣ i ↔ x ^ i = 1 :=
  by
  rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
  · rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
  · rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast, orderOf_dvd_iff_pow_eq_one]

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