cRank_submatrix_le — Mathlib

English

A submatrix obtained by selecting rows/columns has cRank not exceeding that of the original matrix.

Русский

Подматрица, полученная выбором строк/столбцов, имеет cRank не превосходящий cRank исходной матрицы.

LaTeX

$$$\operatorname{cRank}(A_{r,c}) \le \operatorname{cRank}(A).$$$

Lean4

/-- A special case of `lift_cRank_submatrix_le` for when `m₀` and `m` are in the same universe. -/
theorem cRank_submatrix_le {m m₀ : Type um} (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) :
    (A.submatrix r c).cRank ≤ A.cRank := by simpa using lift_cRank_submatrix_le A r c

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