cast_succ

Mathlib.Data.Num.Lemmas

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

English

Casting the successor satisfies cast(succ n) = cast(n) + 1.

Русский

Преобразование преемника удовлетворяет cast(succ n) = cast(n) + 1.

LaTeX

$$$\\forall n \\in \\text{PosNum},\\; \\operatorname{castPosNum}(\\operatorname{succ} n) = \\operatorname{castPosNum}(n) + 1$$$

Lean4

@[simp 500, norm_cast]
theorem cast_succ [AddMonoidWithOne α] (n : PosNum) : (succ n : α) = n + 1 := by rw [← add_one, cast_add, cast_one]

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

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

Разделы

Аффилиация

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