empty_mul

Mathlib.LinearAlgebra.Matrix.Notation

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

English

Repeatedly forming columns from an empty vector yields an empty column again.

Русский

Повторение столбцов из пустого вектора даёт снова пустой столбец.

LaTeX

$$$\\mathrm{replicateCol}\\,\\iota\\, v = \\mathrm{vecEmpty}$, когда $v : \\mathrm{Fin}\\,0 \\to \\alpha$$$

Lean4

@[simp]
theorem empty_mul [Fintype n'] (A : Matrix (Fin 0) n' α) (B : Matrix n' o' α) : A * B = of ![] :=
  empty_eq _

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

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

Разделы

Аффилиация

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