succPNat_coe

Mathlib.Data.PNat.Defs

URI: https://scilib.ai/kg/mathlib#Nat.succPNat_coe

English

The natural-number value of succPNat n is succ n.

Русский

Значение succPNat n в ℕ равно succ n.

LaTeX

$$$ (\\operatorname{succPNat}(n) : \\mathbb{N}) = \\operatorname{succ}(n).$$$

Lean4

@[simp]
theorem succPNat_coe (n : ℕ) : (succPNat n : ℕ) = succ n :=
  rfl

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

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

Разделы

Аффилиация

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