vecMulᵣ — Mathlib

English

vecMulᵣ is the right-acting vector-on-matrix multiplication, equal to the standard vecMul: vecMulᵣ v A = v ᵥ* A.

Русский

vecMulᵣ — правое умножение вектора на матрицу, равно стандартному vecMul: vecMulᵣ v A = v ᵥ* A.

LaTeX

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

Lean4

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

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