zpow_right_inj — Mathlib

English

If a > 1 in a commutative group with a partial order and IsOrderedMonoid, then the map n ↦ a^n is injective on ℤ; i.e., a^m = a^n implies m = n.

Русский

Если a > 1 в коммутативной группе с порядком, то функция n ↦ a^n инъективна на ℤ, то есть a^m = a^n ⇒ m = n.

LaTeX

$$$ [CommGroup \\alpha] [PartialOrder \\alpha] [IsOrderedMonoid \\alpha] {a : \\alpha}, a > 1 \\Rightarrow (a^m = a^n \\iff m = n). $$$

Lean4

@[to_additive zsmul_left_inj]
theorem zpow_right_inj (ha : 1 < a) {m n : ℤ} : a ^ m = a ^ n ↔ m = n :=
  (zpow_right_strictMono ha).injective.eq_iff

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