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_det` in 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_det` in 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)$$

Co-authored-by: Mohanad Ahmed <m.a.m.elhassan@gmail.com>



Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: 3 people

Mathlib/Data/Matrix/Rank.lean

@@ -1,12 +1,13 @@
 /-
 Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Eric Wieer
+Authors: Johan Commelin, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.FreeModule.Finite.Rank
 import Mathlib.LinearAlgebra.Matrix.ToLin
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.LinearAlgebra.Matrix.DotProduct
+import Mathlib.LinearAlgebra.Determinant
 import Mathlib.Data.Complex.Module
 
 #align_import data.matrix.rank from "leanprover-community/mathlib"@"17219820a8aa8abe85adf5dfde19af1dd1bd8ae7"
@@ -101,6 +102,26 @@ theorem rank_of_isUnit [StrongRankCondition R] [DecidableEq n] (A : Matrix n n R
   exact rank_unit A
 #align matrix.rank_of_is_unit Matrix.rank_of_isUnit
 
+/-- Right multiplying by an invertible matrix does not change the rank -/
+lemma rank_mul_eq_left_of_isUnit_det [DecidableEq n]
+    (A : Matrix n n R) (B : Matrix m n R) (hA : IsUnit A.det) :
+    (B ⬝ A).rank = B.rank := by
+  suffices : Function.Surjective A.mulVecLin
+  · rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
+    (LinearMap.range_eq_top.mpr this), ← rank]
+  intro v
+  exact ⟨(A⁻¹).mulVecLin v, by simp [mul_nonsing_inv _ hA]⟩
+
+/-- Left multiplying by an invertible matrix does not change the rank -/
+lemma rank_mul_eq_right_of_isUnit_det [DecidableEq m]
+    (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) :
+    (A ⬝ B).rank = B.rank := by
+  let b : Basis m R (m → R) := Pi.basisFun R m
+  replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by
+    convert hA; rw [← LinearEquiv.eq_symm_apply]; rfl
+  have hAB : mulVecLin (A ⬝ B) = (LinearEquiv.ofIsUnitDet hA).comp (mulVecLin B) := by ext; simp
+  rw [rank, rank, hAB, LinearMap.range_comp, LinearEquiv.finrank_map_eq]
+
 /-- Taking a subset of the rows and permuting the columns reduces the rank. -/
 theorem rank_submatrix_le [StrongRankCondition R] [Fintype m] (f : n → m) (e : n ≃ m)
     (A : Matrix m m R) : rank (A.submatrix f e) ≤ rank A := by