val_ofNat — Mathlib

English

The underlying natural value of the PNAT produced by ofNat(n) is exactly n, i.e., (ofNat(n) : ℕ+) coerced to ℕ equals OfNat.ofNat n.

Русский

Базовое натуральное значение PNAT, полученного из ofNat(n), равно n: (ofNat(n) : ℕ+) при приведение к ℕ равно OfNat.ofNat n.

LaTeX

$$$\forall n:\\mathbb{N}, [NeZero\ n] : ((ofNat(n) : \mathbb{N}^+) : \mathbb{N}) = OfNat.ofNat n$$$

Lean4

@[simp, norm_cast]
theorem val_ofNat (n : ℕ) [NeZero n] : ((ofNat(n) : ℕ+) : ℕ) = OfNat.ofNat n :=
  rfl

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