fromRows_one_isTotallyUnimodular_iff

English

The matrix fromRows with a single all-ones row is TU iff the bottom matrix is TU.

Русский

Матрица fromRows, состоящая из одной строки единиц, TU тогда и только тогда, когда нижняя матрица TU.

LaTeX

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

Lean4

theorem fromRows_one_isTotallyUnimodular_iff [DecidableEq n] (A : Matrix m n R) :
    (fromRows A (1 : Matrix n n R)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular :=
  fromRows_isTotallyUnimodular_iff_rows <| fun h i ↦
    ⟨i, 1, funext fun j ↦ by simp [one_apply, Pi.single_apply, eq_comm]⟩

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