head_fin_const

Mathlib.Data.Fin.VecNotation

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

English

If a vector of length n+1 has all entries equal to a, then its first entry is a.

Русский

Если вектор длины n+1 состоит из одного значения a, то его первая компонента равна a.

LaTeX

$$$\mathrm{vecHead}(\lambda _ : \mathrm{Fin}(n+1) \to \alpha, a) = a$$$

Lean4

@[simp]
theorem head_fin_const (a : α) : (vecHead fun _ : Fin (n + 1) => a) = a :=
  rfl

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

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

Разделы

Аффилиация

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