cast_succ

Mathlib.Data.Nat.Cast.Defs

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

English

For any n ∈ ℕ, the cast of succ n equals n + 1 in R.

Русский

Для любого n ∈ ℕ отображение succ n в R равно n + 1.

LaTeX

$$$ ((\mathrm{succ} \; n) : R) = n + 1 $$$

Lean4

@[norm_cast 500]
theorem cast_succ (n : ℕ) : ((succ n : ℕ) : R) = n + 1 :=
  AddMonoidWithOne.natCast_succ _

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

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

Разделы

Аффилиация

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