zero_mulVec — Mathlib

English

For any vector v, 0 ×ᵥ v = 0; i.e., the result is the zero vector when multiplying by the zero matrix on the left.

Русский

Для любого вектора v произведение 0 ×ᵥ v равно 0; т.е. результат нулевой вектор при умножении слева нулевой матрицей.

LaTeX

$$$0 ᵥ* v = 0$$$

Lean4

@[simp]
theorem zero_mulVec [Fintype n] (v : n → α) : (0 : Matrix m n α) *ᵥ v = 0 :=
  by
  ext
  simp [mulVec]

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