zpow_eq_zpow_iff_modEq — Mathlib

English

For any m,n ∈ Z, x^m = x^n iff m ≡ n (mod orderOf x).

Русский

Для любых m,n ∈ Z, x^m = x^n тогда и только тогда, когда m ≡ n (mod orderOf x).

LaTeX

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

Lean4

@[to_additive]
theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x] := by
  rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd, zero_sub, neg_sub]

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