rank_submatrix — Mathlib

English

Reindexing-based submatrix has the same rank as the original: rank(A.submatrix em en) = rank A.

Русский

Подматрица, полученная перестановкой индексов, имеет тот же ранг, что и исходная: rank(A.submatrix em en) = rank A.

LaTeX

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

Lean4

@[simp]
theorem rank_submatrix [Fintype n₀] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
    rank (A.submatrix em en) = rank A := by simpa only [reindex_apply] using rank_reindex em.symm en.symm A

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