toList_nil

Mathlib.Data.Vector.Defs

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

English

The nil vector maps to the empty list: toList nil = List.nil.

Русский

Пустой вектор отображается в пустой список: toList nil = List.nil.

LaTeX

$$@[simp]\\ntheorem toList_nil : toList nil = @List.nil α$$

Lean4

/-- A nil vector maps to a nil list. -/
@[simp]
theorem toList_nil : toList nil = @List.nil α :=
  rfl

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

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

Разделы

Аффилиация

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