Commit 2025-06-21 09:25 17eb7da2

View on Github →

feat(Data/Matrix): Matrix.fromRows_map and Matrix.fromCols_map (#26222) The new lemmas Matrix.fromRows_map and Matrix.fromCols_map are analogous to Matrix.fromBlocks_map.

Estimated changes

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

added theorem Matrix.fromCols_map

added theorem Matrix.fromRows_map