Commit 2026-04-09 10:59 aa41e0b2

feat: generalize rank_submatrix_le to arbitrary column maps (#37000) This PR generalizes rank_submatrix_le to allow an arbitrary function on columns instead of requiring an Equiv. The previous version required e : m₀ ≃ m and [Fintype m], while this version only requires c : n₀ → n and [Fintype n₀]. The previous version can be recovered as a special case of the new one.