pow_eq_pow_iff_modEq — Mathlib

English

For a LeftCancelMonoid, x^n = x^m iff n ≡ m mod orderOf x.

Русский

В левознаменованном моноиде: x^n = x^m тогда и только тогда, когда n ≡ m mod orderOf(x).

LaTeX

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

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 [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]
  exact ⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩

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