English
Left multiplication by a fixed vector defines an AddMonoidHom: v ↦ (M *ᵥ v).
Русский
Левое умножение на фиксированный вектор задаёт гомоморфизм AddMonoid: v ↦ M *ᵥ v.
LaTeX
$$AddMonoidHom Left$$
Lean4
/-- `v ᵥ* M` (notation for `vecMul v M`) is the vector-matrix product of vector `v` and matrix `M`,
where `v` is seen as a row vector.
Put another way, `v ᵥ* M` is the vector whose entries are those of `row v * M` (see `row_vecMul`).
The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `dotProduct`,
so that `v ᵥ* A ⬝ᵥ w ᵥ* B` is parsed as `(v ᵥ* A) ⬝ᵥ (w ᵥ* B)`.
-/
def vecMul [Fintype m] (v : m → α) (M : Matrix m n α) : n → α
| j => v ⬝ᵥ fun i => M i j
