vecMul_zero

Mathlib.Data.Matrix.Mul

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

English

The matrix-vector product distributes over vector addition: A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y.

Русский

Произведение матрицы и вектора распределяется по сложению векторов: A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y.

LaTeX

$$$A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y$$$

Lean4

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

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

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

Разделы

Аффилиация

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