orderOf_dvd_sub_iff_zpow_eq_zpow — Mathlib

English

For any x in a group and any integer i, the divisibility (orderOf x) ∣ i is equivalent to x^i = 1; this holds for both nonnegative and negative i with the appropriate interpretation of x^i.

Русский

Для любого x в группе и любого целого i делимость (orderOf x) ∣ i эквивалентна x^i = 1; это справедливо и для отрицательных i при правильной трактовке x^i.

LaTeX

$$$(\\operatorname{orderOf} x) \\mid i \\;\\Leftrightarrow\\; x^i = 1$$

Lean4

@[to_additive]
theorem orderOf_dvd_sub_iff_zpow_eq_zpow {a b : ℤ} : (orderOf x : ℤ) ∣ a - b ↔ x ^ a = x ^ b := by
  rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]

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