Commit 2025-02-26 21:00 2bda65d5

View on Github →

feat: generalize rank_reindex to rectangular matrices (#22277)

Estimated changes

Modified Mathlib/Data/Matrix/Rank.lean

modified theorem Matrix.rank_reindex

modified theorem Matrix.rank_submatrix