Commit 2026-06-08 10:43 dd7fc3b3

View on Github →

refactor(LinearAlgebra/Matrix/Rank): generalize Matrix.rank/LinearMap.rank to semirings (#39158)

  • Generalize Matrix.rank from CommRing to CommSemiring
  • Generalize LinearMap.rank from AddCommGroups over Rings to AddCommMonoids over Semirings (which are the minimum requirements for Module)
  • Many Matrix.rank theorems now require StrongRankCondition explicitly (which CommRing used to provide)
  • Matrix.cRank theorems don't need commutativity

Estimated changes

modified theorem Matrix.cRank_one
modified theorem Matrix.cRank_reindex
modified theorem Matrix.cRank_submatrix
modified theorem Matrix.cRank_toNat_eq_rank
modified theorem Matrix.cRank_zero
modified theorem Matrix.eRank_one
modified theorem Matrix.eRank_reindex
modified theorem Matrix.eRank_submatrix
modified theorem Matrix.eRank_toNat_eq_rank
modified theorem Matrix.eRank_zero
modified theorem Matrix.lift_cRank_reindex
modified theorem Matrix.lift_cRank_submatrix
modified theorem Matrix.rank_le_card_height
modified theorem Matrix.rank_le_card_width
modified theorem Matrix.rank_le_height
modified theorem Matrix.rank_le_width
modified theorem Matrix.rank_mul_le
modified theorem Matrix.rank_mul_le_left
modified theorem Matrix.rank_mul_le_right
modified theorem Matrix.rank_of_isUnit
modified theorem Matrix.rank_one
modified theorem Matrix.rank_reindex
modified theorem Matrix.rank_submatrix
modified theorem Matrix.rank_submatrix_le
modified theorem Matrix.rank_subsingleton
modified theorem Matrix.rank_unit
modified theorem Matrix.rank_vecMulVec_le
modified theorem Matrix.rank_zero