Commit 2025-03-18 15:42 d90da06b

feat(Matrix): rank of infinite matrices (#22226) This PR is the first in a series that attempts to improve generality in the current API for matrix rank. At the moment, for A : Matrix m n R, the term A.rank is only well-defined for Fintype n and CommRing R. This is because the definition is in terms of MulVecLin, which requires these typeclass assumptions. The Fintype assumption, especially, is a little unfortunate, since it necessitates unnecessary and column/row-asymmetric Fintype assumptions throughout the API, and makes it impossible to state the important lemma rank_transpose for infinite matrices. We don't touch the current definition Matrix.rank directly here, but we introduce cardinal and ENat-valued notions of rank for infinite matrices, with basic API for monotonicity. The lemma cRank_toNat_eq_rank is a proof of concept - it shows that the current Matrix.rank could easily be redefined as Matrix.rank A := (Matrix.cRank A).toNat with a strict gain in generality, and no loss to the existing API. The plan is to do this, and thereby prove rank_transpose in greater generality, in coming PRs. The definition Matrix.eRank is also natural, since Matrix.eRank_transpose will be true, but Matrix.cRank_transpose will not. Zulip thread