Theorems · Definition · linear algebra

Matrix.vecMulVec

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

For two vectors w and v, vecMulVec w v i j is defined to be w i * v j. Put another way, vecMulVec w v is exactly replicateCol ι w * replicateRow ι v for Unique ι; see vecMulVec_eq.

Defined in

Mathlib.Data.Matrix.Mul

Cited by

52 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

Mul