ofVector_nil

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.ofVector_nil

English

The vector nil coerces to the Sym nil element.

Русский

Векторный нуль отображается в элемент Sym α 0, равный nil.

LaTeX

$$$ \uparrow(\operatorname{Vector.nil}) = \operatorname{Sym.nil}$$$

Lean4

@[simp]
theorem ofVector_nil : ↑(Vector.nil : List.Vector α 0) = (Sym.nil : Sym α 0) :=
  rfl

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

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

Разделы

Аффилиация

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