fromCols_replicateCol0_isTotallyUnimodular_iff

English

The equivalence: (fromCols A (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular.

Русский

Эквивалентность: (fromCols A (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular.

LaTeX

$$(fromCols A (replicateCol n' 0)).IsTotallyUnimodular \\iff A.IsTotallyUnimodular$$

Lean4

theorem fromCols_replicateCol0_isTotallyUnimodular_iff (A : Matrix m n R) :
    (fromCols A (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular := by
  rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

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