coe_toPNat'

Mathlib.Data.PNat.Defs

URI: https://scilib.ai/kg/mathlib#PNat.coe_toPNat'

English

For n ∈ ℕ^+, the equality (n.val).toPNat' = n holds.

Русский

Для n ∈ ℕ^+, равенство (n.val).toPNat' = n выполняется.

LaTeX

$$$ (n \\in \\mathbb{N}^+) \\;:\\; (n.\\text{val}).toPNat' = n.$$$

Lean4

@[simp]
theorem coe_toPNat' (n : ℕ+) : (n : ℕ).toPNat' = n :=
  eq (toPNat'_coe n.pos)

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

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

Разделы

Аффилиация

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