eRank_reindex

Mathlib.LinearAlgebra.Matrix.Rank

URI: https://scilib.ai/kg/mathlib#Matrix.eRank_reindex

← MathLib Explorer

English

Reindexing preserves the eRank: eRank(A.reindex em en) = eRank(A).

Русский

Переиндексация сохраняет eRank: eRank(A.reindex em en) = eRank(A).

LaTeX

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

Lean4

theorem eRank_reindex {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) :
    eRank (A.reindex em en) = eRank A :=
  eRank_submatrix ..

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru