Theorem Matrix.toColumns₁_fromColumns

Modification history

2024-02-09 19:37

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

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

Modified Matrix.toColumns₁_fromColumns View on Github →

2023-08-02 13:41

Mathlib/Data/Matrix/ColumnRowPartitioned.lean

feat: column and row partitioned matrices (#6052) …

Added Matrix.toColumns₁_fromColumns View on Github →