fromRows_replicateRow0_isTotallyUnimodular_iff

English

The equivalence: (fromRows A (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular.

Русский

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

LaTeX

$$(fromRows A (replicateRow m' 0)).IsTotallyUnimodular \\iff A.IsTotallyUnimodular$$

Lean4

theorem fromRows_replicateRow0_isTotallyUnimodular_iff (A : Matrix m n R) :
    (fromRows A (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular := by
  classical
  refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]

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