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