cRank_submatrix — Mathlib

English

The cRank of a submatrix equals the cRank of the original matrix (in the same universe).

Русский

cRank подматрицы равен cRank исходной матрицы (в той же вселенной).

LaTeX

$$$cRank(A_{\text{submatrix em en}}) = cRank(A)$$$

Lean4

/-- A special case of `lift_cRank_submatrix` for when the row types are in the same universe. -/
@[simp]
theorem cRank_submatrix {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
    cRank (A.submatrix em en) = cRank A := by simpa [-lift_cRank_submatrix] using A.lift_cRank_submatrix em en

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