smul_eq_mulVec

Mathlib.Data.Matrix.Action

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

English

The scalar action on a column vector given by a matrix equals the matrix-vector product; i.e., A • v = A *ᵥ v.

Русский

Умножение матрицы на вектор-столбец через скалярное умножение эквивалентно произведению матрица-вектор.

LaTeX

$$$A \cdot v = A \ast v$$$

Lean4

@[simp]
theorem smul_eq_mulVec (A : Matrix n n R) (v : n → R) : A • v = A *ᵥ v :=
  rfl

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

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

Разделы

Аффилиация

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