zpow_right_inj₀ — Mathlib

English

If 0 < a and a ≠ 1, then the exponential map n ↦ a^n is injective.

Русский

Если 0 < a и a ≠ 1, то экспоненциальное отображение n ↦ a^n инъективно.

LaTeX

$$$\forall a\in G_0,\ 0 < a \land a \neq 1 \Rightarrow \forall m,n \in \mathbb{Z},\ a^m = a^n \Rightarrow m = n$$$

Lean4

@[simp]
theorem zpow_right_inj₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
  (zpow_right_injective₀ ha₀ ha₁).eq_iff

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