English
Left multiplication by a matrix defines an AddMonoidHom from matrices to vectors: M ↦ M *ᵥ v.
Русский
Левое умножение матрицы задаёт гомоморфизм добавочных моноидов: M ↦ M *ᵥ v.
LaTeX
$$AddMonoidHom\\big(\\mathrm{Matrix}_{m,n}(\\alpha)\\to\\alpha^m\\big)(M) = M *ᵥ v$$
Lean4
/-- `M *ᵥ v` (notation for `mulVec M v`) is the matrix-vector product of matrix `M` and vector `v`,
where `v` is seen as a column vector.
Put another way, `M *ᵥ v` is the vector whose entries are those of `M * col v` (see `col_mulVec`).
The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `dotProduct`,
so that `A *ᵥ v ⬝ᵥ B *ᵥ w` is parsed as `(A *ᵥ v) ⬝ᵥ (B *ᵥ w)`.
-/
def mulVec [Fintype n] (M : Matrix m n α) (v : n → α) : m → α
| i => (fun j => M i j) ⬝ᵥ v
