empty_mulVec — Mathlib

English

Let α be a nonunital nonassoc semiring. If A is a matrix with Fin 0 rows and any number of columns, and v is any vector, then A mulVec v equals the zero vector (vecEmpty).

Русский

Пусть α — неединичное неассоциативное полукольцо. Пусть A — матрица размера 0 × n', и v — любой вектор, тогда A mulVec v равно нулевому вектору (vecEmpty).

LaTeX

$$$A \mulVec v = 0$ for $A : \mathrm{Matrix}(\mathrm{Fin}~0, n', \alpha)$ and $v : \mathrm{Fin}~0 \to \alpha$.$$

Lean4

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

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