Theorem Matrix.submatrix_id_mul_right

Modification history

2024-11-28 16:12
Mathlib/Data/Matrix/Mul.lean
feat: drop finite-dimensionality assumption from `PerfectPairing.restrictScalarsField` (#18940)
Added Matrix.submatrix_id_mul_rightView on Github →