Commit 2025-07-13 18:42 8608bbd8

View on Github →

feat: allow trivial rings in Matrix.rank_mul_le (#27074) Now that the instance from CommRing to StrongRankCondition is imported, we can weaken to Nontrivial. nontriviality can then eliminate this assumption from some later lemmas.

Estimated changes

modified theorem Matrix.cRank_one
modified theorem Matrix.eRank_one
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_submatrix_le
modified theorem Matrix.rank_unit