coe_ofNat — Mathlib

English

The hyperreal image of a natural number agrees with the standard embedding of natural numbers into hyperreals.

Русский

Гиперреальный образ натурального числа совпадает со стандартным вложением натуральных чисел в гиперреалы.

LaTeX

$$$((\mathrm{ofNat}(n) : \mathbb{R})^{\\*}) = \mathrm{OfNat.ofNat}(n)$$$

Lean4

@[simp, norm_cast]
theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ) : ℝ*) = OfNat.ofNat n :=
  rfl

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