pow_left_injective

Mathlib.Data.Nat.Basic

URI: https://scilib.ai/kg/mathlib#Nat.pow_left_injective

English

For n ≠ 0, the map a ↦ a^n is injective on ℕ.

Русский

При n ≠ 0 отображение a ↦ a^n на ℕ инъективно.

LaTeX

$$$\forall a,b,n \in \mathbb{N},\; n \neq 0 \Rightarrow a^{n}=b^{n} \Rightarrow a=b$$$

Lean4

theorem pow_left_injective (hn : n ≠ 0) : Injective (fun a : ℕ ↦ a ^ n) := by
  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_left hn]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru