mulVecᵣ — Mathlib

English

mulVecᵣ is the row-vector times matrix product, i.e., it equals the standard row-vector matrix multiplication: mulVecᵣ v A = v ⬝ A.

Русский

mulVecᵣ есть произведение строкового вектора на матрицу: mulVecᵣ v A = v ⬝ A.

LaTeX

$$$\\text{mulVec}ᵣ \\; v \\; A = v \\; ᵥ*\\; A$$$

Lean4

/-- `Matrix.mulVec` with better defeq for `Fin` -/
def mulVecᵣ [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α) : Fin l → α :=
  FinVec.map (fun a => dotProductᵣ a v) A

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