Theorem Matrix.fromRows_map

Modification history

2025-06-21 09:25
Mathlib/Data/Matrix/ColumnRowPartitioned.lean
feat(Data/Matrix): `Matrix.fromRows_map` and `Matrix.fromCols_map` (#26222) …
Added Matrix.fromRows_mapView on Github →