Theorems · Definition · linear algebra

Matrix.vecMul

{m : Type u_2} →
  {n : Type u_3} → {α : Type v} → [NonUnitalNonAssocSemiring α] → [Fintype m] → (m → α) → Matrix m n α → n → α

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. The notation has precedence 73, which comes immediately before ⬝ᵥ for dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

Defined in

Mathlib.Data.Matrix.Mul

Cited by

148 results in Mathlib

Foundations

Depth 15 from the axioms, rests on 104 definitions · uses propext, Quot.sound

Assumes

NonUnitalNonAssocSemiringFintype