Theorem Matrix.dotProduct_transpose_mulVec

Modification history

2026-07-01 17:54
Mathlib/Data/Matrix/Mul.lean
feat(LinearAlgebra/Matrix/Nondegenerate): more API and generalize to non-domains (#39634) …
Modified Matrix.dotProduct_transpose_mulVecView on Github →
2026-05-01 15:28
Mathlib/Data/Matrix/Mul.lean
feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations (#34851) …
Added Matrix.dotProduct_transpose_mulVecView on Github →