rank_reindex — Mathlib

English

Reindexing the rows and columns by bijections does not change the rank: rank(A.reindex em en) = rank(A).

Русский

Изменение индексов строк и столбцов по биекциям не изменяет ранг: rank(A.reindex em en) = rank(A).

LaTeX

$$$\operatorname{rank}(A^{\text{reindex }(em,en)}) = \operatorname{rank}(A)$$$

Lean4

theorem rank_reindex [Fintype n₀] (em : m ≃ m₀) (en : n ≃ n₀) (A : Matrix m n R) : rank (A.reindex em en) = rank A := by
  rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, Submodule.map_top,
    LinearEquiv.finrank_map_eq]

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