reindex — Mathlib

English

Reindexing a matrix by bijections on the row and column indices preserves total unimodularity.

Русский

Переиндексация по биекциям строк и столбцов сохраняет тотальную унимодулярность.

LaTeX

$$(A.reindex em en).IsTotallyUnimodular$$

Lean4

theorem reindex {A : Matrix m n R} (em : m ≃ m') (en : n ≃ n') (hA : A.IsTotallyUnimodular) :
    (A.reindex em en).IsTotallyUnimodular :=
  hA.submatrix _ _

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