ofNat_inj

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.ofNat_inj

English

For m,n ∈ ℕ with NeZero, (ofNat m : ℕ+) = ofNat n ↔ m = n.

Русский

Для m,n ∈ ℕ с NeZero: (ofNat m : ℕ+) = ofNat n ↔ m = n.

LaTeX

$$$(\\\\operatorname{ofNat} m : \\\\mathbb{N}^+) = \\\\-operatorname{ofNat} n \\\\iff m = n.$$$

Lean4

@[simp]
theorem ofNat_inj {m n : ℕ} [NeZero m] [NeZero n] : (ofNat(m) : ℕ+) = ofNat(n) ↔ OfNat.ofNat m = OfNat.ofNat n :=
  Subtype.mk_eq_mk

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

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

Разделы

Аффилиация

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