English
If A is invertible, then rank(AB) = rank(B) for any B of appropriate size.
Русский
Если A обратима, то для любого B ранг(AB) = ранг(B).
LaTeX
$$$\text{If } \det A \text{ is a unit, then } \operatorname{rank}(AB)=\operatorname{rank}(B)$$$
Lean4
/-- Left multiplying by an invertible matrix does not change the rank -/
@[simp]
theorem rank_mul_eq_right_of_isUnit_det [Fintype m] [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]
