mulVec_add

Mathlib.Data.Matrix.Mul

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

English

The matrix-vector product is linear in the vector: A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y.

Русский

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

LaTeX

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

Lean4

theorem mulVec_add [Fintype n] (A : Matrix m n α) (x y : n → α) : A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y :=
  by
  ext
  apply dotProduct_add

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

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

Разделы

Аффилиация

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