Theorems · Definition · linear algebra

Matrix.mulVec

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

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

Defined in

Mathlib.Data.Matrix.Mul

Cited by

267 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringFintype