coe_inj — Mathlib

English

The coercion from ℕ+ to ℕ is injective: (m : ℕ) = n ⇔ m = n.

Русский

Приведение из ℕ+ в ℕ инъективно: (m : ℕ) = n ⇔ m = n.

LaTeX

$$$ (m : \\\\mathbb{N}) = n \\\\iff m = n $$$

Lean4

/-- We now define a long list of structures on `ℕ+` induced by
similar structures on `ℕ`. Most of these behave in a completely
obvious way, but there are a few things to be said about
subtraction, division and powers.
-/
@[simp, norm_cast]
theorem coe_inj {m n : ℕ+} : (m : ℕ) = n ↔ m = n :=
  SetCoe.ext_iff

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