Theorem Matrix.fromColumns_mulVec_sum_elim

Modification history

2024-08-07 07:08

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

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

Modified Matrix.fromColumns_mulVec_sum_elim 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.fromColumns_mulVec_sum_elim View on Github →