one_fromRows_isTotallyUnimodular_iff

English

The equivalence: (fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular.

Русский

Эквивалентность: (fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular.

LaTeX

$$(fromRows A 1).IsTotallyUnimodular \\iff A.IsTotallyUnimodular$$

Lean4

theorem one_fromRows_isTotallyUnimodular_iff [DecidableEq n] (A : Matrix m n R) :
    (fromRows (1 : Matrix n n R) A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular :=
  by
  have hA :
    fromRows (1 : Matrix n n R) A = (fromRows A (1 : Matrix n n R)).reindex (Equiv.sumComm m n) (Equiv.refl n) := by
    aesop
  rw [hA, reindex_isTotallyUnimodular, fromRows_one_isTotallyUnimodular_iff]

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