vecHead_vecAlt0

Mathlib.Data.Fin.VecNotation

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

English

The head (first element) of vecAlt0 is the first element of the original vector.

Русский

Голова (первый элемент) vecAlt0 равна первому элементу исходного вектора.

LaTeX

$$$\\operatorname{vecHead}(\\operatorname{vecAlt0}\\, hm\\, v) = v(0)$$$

Lean4

@[simp]
theorem vecHead_vecAlt0 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : vecHead (vecAlt0 hm v) = v 0 :=
  rfl

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

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

Разделы

Аффилиация

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