Commit 2025-07-05 02:43 cca0ea3a
View on Github →fix (Data/Matrix/Rank): extend applicability of rank_submatrix_le (#26536)
The current version of rank_submatrix_le is restricted to square matrices and doesn't allow for the reduction of lines. Both restrictions can be removed easily without changing the proof.