cons_val_zero'

Mathlib.Data.Fin.VecNotation

URI: https://scilib.ai/kg/mathlib#Matrix.cons_val_zero'

English

For the index ⟨0, h⟩, the value of vecCons x u at that index is x.

Русский

Для индекса ⟨0, h⟩ значение vecCons x u в этом индексе равно x.

LaTeX

$$$\mathrm{vecCons} x u \langle 0, h \rangle = x$$$

Lean4

theorem cons_val_zero' (h : 0 < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨0, h⟩ = x :=
  rfl

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

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

Разделы

Аффилиация

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