Theorem Matrix.submatrix_id_mul_left

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_leftView on Github →