reindex_isTotallyUnimodular — Mathlib

English

Equivalence: A reindexed matrix is totally unimodular iff the original matrix is.

Русский

Эквивалентность: переставленная по индексам матрица тотально унимодулярна тогда и только тогда, когда исходная матрица тоже такова.

LaTeX

$$AIsTotallyUnimodular \\iff A.reindex em en.IsTotallyUnimodular$$

Lean4

theorem reindex_isTotallyUnimodular (A : Matrix m n R) (em : m ≃ m') (en : n ≃ n') :
    (A.reindex em en).IsTotallyUnimodular ↔ A.IsTotallyUnimodular :=
  ⟨fun hA => by simpa [Equiv.symm_apply_eq] using hA.reindex em.symm en.symm, fun hA => hA.reindex _ _⟩

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