English
Taking a submatrix by selecting some rows and permuting columns cannot increase rank: rank(A_sub) ≤ rank(A).
Русский
Взятие подматрицы по выбору некоторого набора строк и перестановке столбцов не может увеличить ранг: rank(A_sub) ≤ rank(A).
LaTeX
$$$\operatorname{rank}(A_{\text{submatrix}}) \le \operatorname{rank}(A)$$$
Lean4
/-- Taking a subset of the rows and permuting the columns reduces the rank. -/
theorem rank_submatrix_le [Nontrivial R] [Fintype m] [Fintype m₀] (f : n₀ → n) (e : m₀ ≃ m) (A : Matrix n m R) :
rank (A.submatrix f e) ≤ rank A :=
by
rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
show LinearMap.funLeft R R e.symm = LinearEquiv.funCongrLeft R R e.symm from rfl, LinearEquiv.range,
Submodule.map_top]
exact Submodule.finrank_map_le _ _
