zpow_right_injective₀ — Mathlib

English

If 0 < a and a ≠ 1, then the map n ↦ a^n from the integers to the group 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

theorem zpow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective fun n : ℤ ↦ a ^ n :=
  by
  obtain ha₁ | ha₁ := ha₁.lt_or_gt
  · exact (zpow_right_strictAnti₀ ha₀ ha₁).injective
  · exact (zpow_right_strictMono₀ ha₁).injective

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