eRank_submatrix — Mathlib

English

The eRank of a submatrix equals the eRank of the original matrix: eRank(A.submatrix em en) = eRank(A).

Русский

eRank подматрицы равен eRank исходной матрицы: eRank(A.submatrix em en) = eRank(A).

LaTeX

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

Lean4

@[simp]
theorem eRank_submatrix {n : Type un} (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
    eRank (A.submatrix em en) = eRank A := by
  simpa [-lift_cRank_submatrix] using congr_arg Cardinal.toENat <| A.lift_cRank_submatrix em en

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