pow_inj_mod — Mathlib

English

For a LeftCancelMonoid, x^n = x^m iff n ≡ m mod orderOf x; equivalently, the map n ↦ x^n is injective iff x has infinite order.

Русский

Для левоотменимого моноида: x^n = x^m эквивалентно n ≡ m mod orderOf(x); отображение инъективно тогда, когда orderOf(x) бесконечен.

LaTeX

$$Injective (n ↦ x^n) ⇔ ¬IsOfFinOrder(x)$$

Lean4

@[to_additive]
theorem pow_inj_mod {n m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x :=
  hx.pow_eq_pow_iff_modEq

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