mk_ofNat — Mathlib

English

If n > 0, then the canonical builder ⟨ofNat(n), proof⟩ in ℕ+ equals the standard OfNat.ofNat n.

Русский

Если n > 0, то канонический конструктор ⟨ofNat(n), доказательство⟩ в ℕ+ равен стандартному OfNat.ofNat n.

LaTeX

$$$@[simp]\; (n : \mathbb{N})\, (h:0

Lean4

@[simp]
theorem mk_ofNat (n : ℕ) (h : 0 < n) :
    @Eq ℕ+ (⟨ofNat(n), h⟩ : ℕ+)
      (haveI : NeZero n := ⟨h.ne'⟩;
      OfNat.ofNat n) :=
  rfl

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