replicateCol_empty

Mathlib.LinearAlgebra.Matrix.Notation

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

English

The column-wise replication of a zero-length vector results in an empty column vector.

Русский

Повторение столбца нулевой длины дает пустой столбец.

LaTeX

$$$\\mathrm{replicateCol}\\,\\iota\\, v = \\mathrm{vecEmpty}$ for $v : \\mathrm{Fin}\\,0 \\to \\alpha$$$

Lean4

@[simp]
theorem replicateCol_empty (v : Fin 0 → α) : replicateCol ι v = vecEmpty :=
  empty_eq _

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

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

Разделы

Аффилиация

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