repeat_eq_nil

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.repeat_eq_nil

English

The type-level equality repeatEq α equals nilFun when α has length 0.

Русский

Типовое равенство repeatEq α равно nilFun, когда α имеет длину 0.

LaTeX

$$$$\\text{repeatEq}(\\alpha) = \\text{nilFun}.$$$$

Lean4

@[typevec]
theorem repeat_eq_nil (α : TypeVec 0) : repeatEq α = nilFun := by ext i; cases i

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

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

Разделы

Аффилиация

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