rank_mul_eq_left_of_isUnit_det — Mathlib

English

If A is invertible, then rank(BA) = rank(B) for any B of appropriate size.

Русский

Если A обратима, то для любого B матричное произведение BA сохраняет ранг: ранг(BA) = ранг(B).

LaTeX

$$$\text{If } \det A \text{ is a unit, then } \operatorname{rank}(BA)=\operatorname{rank}(B)$$$

Lean4

/-- Right multiplying by an invertible matrix does not change the rank -/
@[simp]
theorem 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 by
    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]⟩

Похожие утверждения