Commit 2023-08-03 20:55 067bc406
View on Github →feat: (Mathlib.Data.Matrix.Rank): rank of a matrix unaffected by multiplication with invertible matrices (#6051) This PR provides two lemmas:
Matrix.rank_mul_eq_left_of_isUnit_detin a commutative ring R post multiplication (multiplication from the right) by an invertible matrix does not change the rank of a matrix. With $A$ an invertible matrix: $$\text{rank}(BA) = \text{rank}(B)$$Matrix.rank_mul_eq_right_of_isUnit_detin a commutative ring R pre-multiplication (multiplication from the left) by an invertible matrix does not change the rank of a matrix. With $A$ an invertible matrix: $$\text{rank}(AB) = \text{rank}(B)$$