empty_vecMul — Mathlib

English

Let α be a nonunital, nonassociative semiring. If v is the empty row vector in α^{Fin 0} and B is a matrix with 0 rows and o' columns, then the product v ᵥ* B is the zero vector in α^{o'}.

Русский

Пусть α — немонолитное неассоциативное полукольцо без единицы. Пусть v — пустой вектор-строка длины 0, а B — матрица размера 0 × o'. Тогда произведение v ᵥ* B равно нулю в α^{o'}.

LaTeX

$$$\mathrm{vecMul}(v,B)=0_{o'}$, where $v:\alpha^{0}$ and $B:\alpha^{0\times o'}$.$$

Lean4

@[simp]
theorem empty_vecMul (v : Fin 0 → α) (B : Matrix (Fin 0) o' α) : v ᵥ* B = 0 :=
  rfl

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