toList_cons

Mathlib.Data.Vector.Defs

URI: https://scilib.ai/kg/mathlib#List.Vector.toList_cons

← MathLib Explorer

English

toList of cons a v is the same as a :: toList v.

Русский

toList (cons a v) = a :: toList v.

LaTeX

$$@[simp]\\ntheorem toList_cons (a : α) (v : Vector α n) : toList (cons a v) = a :: toList v$$

Lean4

/-- `toList` of `cons` of a vector and an element is
the `cons` of the list obtained by `toList` and the element -/
@[simp]
theorem toList_cons (a : α) (v : Vector α n) : toList (cons a v) = a :: toList v := by cases v; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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