Theorem Matrix.fromCols_mulVec

Modification history

2025-09-22 13:29
Mathlib/Data/Matrix/ColumnRowPartitioned.lean
feat(Data/Matrix): add `vecMul_fromRows` and `fromCols_mulVec` (#29784) …
Added Matrix.fromCols_mulVecView on Github →