Theorem Matrix.vecMul_fromColumns

Modification history

2024-08-07 07:08

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

chore: backports for leanprover/lean4#4814 (part 22) (#15511)

Modified Matrix.vecMul_fromColumns View on Github →

2024-02-09 19:37

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

feat: `Matrix.fromRows` and `Matrix.fromColumns` multiplied by vectors (#10379) …

Added Matrix.vecMul_fromColumns View on Github →