feat(Matrix): rank of infinite matrices

[apnelson1]

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

---

[github-actions]

PR summary 92831e7b26

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ cRank
+ cRank_le_card_col
+ cRank_le_card_row
+ cRank_lift_mono_row.{u,u₀,v}
+ cRank_mono_col
+ cRank_mono_row.{u}
+ cRank_toNat_eq_finrank
+ cRank_toNat_eq_rank
+ eRank
+ eRank_le_card_col
+ eRank_le_card_row
+ eRank_submatrix_le
+ eRank_toNat_eq_finrank

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).