vecHead_vecAlt1

Mathlib.Data.Fin.VecNotation

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

English

The head of vecAlt1 is the second element of the original vector.

Русский

Голова vecAlt1 равна второму элементу исходного вектора.

LaTeX

$$$\\operatorname{vecHead}(\\operatorname{vecAlt1}\\, hm\\, v) = v(1)$$$

Lean4

@[simp]
theorem vecHead_vecAlt1 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : vecHead (vecAlt1 hm v) = v 1 := by
  simp [vecHead, vecAlt1]

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

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

Разделы

Аффилиация

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