pow_eq_pow_iff_modEq — Mathlib

English

For prime p, if not x^{p^n} = 1 and x^{p^{n+1}} = 1, then orderOf(x) = p^{n+1}.

Русский

Для простого p: если не выполняется x^{p^n}=1, но выполняется x^{p^{n+1}}=1, тогда orderOf(x) = p^{n+1}.

LaTeX

$$\neg (x^{p^n} = 1) \wedge (x^{p^{n+1}} = 1) \Rightarrow \operatorname{orderOf}(x) = p^{n+1}$$

Lean4

@[to_additive]
theorem pow_eq_pow_iff_modEq : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x] :=
  by
  wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
  exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩

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