Theorem Matrix.vecMul_fromRows

Modification history

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