vecMul_empty — Mathlib

English

Let α be a nonunital, nonassociative semiring. If v is any vector in α^{n'} and B is a matrix in α^{n'×Fin 0}, then the product v ᵥ* B is the empty vector (zero-length).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem vecMul_empty [Fintype n'] (v : n' → α) (B : Matrix n' (Fin 0) α) : v ᵥ* B = ![] :=
  empty_eq _

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