vecHead

Mathlib.Data.Fin.VecNotation

URI: https://scilib.ai/kg/mathlib#Matrix.vecHead

English

vecHead v gives the first entry of the vector v, i.e., vecHead v = v(0).

Русский

vecHead v даёт первый элемент вектора v: vecHead v = v(0).

LaTeX

$$$\\operatorname{vecHead} (v) = v(0)$$$

Lean4

/-- `vecHead v` gives the first entry of the vector `v` -/
def vecHead {n : ℕ} (v : Fin n.succ → α) : α :=
  v 0

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

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

Разделы

Аффилиация

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