get_zero

Mathlib.Data.Vector.Basic

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

English

For any vector v of length n+1, the 0-th element equals the head of v.

Русский

Для любого вектора v длины n+1 нулевой элемент равен голове вектора.

LaTeX

$$$\\forall \\alpha\\;\\forall n\\;\\forall v:\\mathrm{Vector}\\ \\alpha\\ (n+1),\\; \\mathrm{get}(v,0) = \\mathrm{head}(v)$$$

Lean4

@[simp]
theorem get_zero : ∀ v : Vector α n.succ, get v 0 = head v
  | ⟨_ :: _, _⟩ => rfl

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

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

Разделы

Аффилиация

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