cast_succ

Mathlib.Data.Num.ZNum

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

English

For any n in ZNum, the image of succ n equals n+1 in α.

Русский

Для любого n ∈ ZNum образ succ n равен n+1 в α.

LaTeX

$$$$\forall n \in ZNum,\ ((succ\ n : ZNum) : α) = (n : α) + 1.$$$$

Lean4

@[simp]
theorem cast_succ [AddGroupWithOne α] (n) : ((succ n : ZNum) : α) = n + 1 := by rw [← add_one, cast_add, cast_one]

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

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

Разделы

Аффилиация

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