theorem Matrix.IsTotallyUnimodular.comp_rows {X₁ X₂ Z R : Type} [CommRing R] {A : Matrix X₁ X₂ R} (hA : A.IsTotallyUnimodular) (e : Z → X₁) : Matrix.IsTotallyUnimodular (A ∘ e)

theorem Matrix.IsTotallyUnimodular.comp_cols {X₁ X₂ Z R : Type} [CommRing R] {A : Matrix X₁ X₂ R} (hA : A.IsTotallyUnimodular) (e : Z → X₂) : Matrix.IsTotallyUnimodular fun (x : X₁) => A x ∘ e

noncomputable instance instFintypeSubtypeProdEqSumFstInlSnd_seymour {X₁ X₂ Z : Type} [Fintype Z] {f : Z → X₁ ⊕ X₂} : Fintype { x₁ : Z × X₁ // f x₁.1 = Sum.inl x₁.2 }

Equations

• instFintypeSubtypeProdEqSumFstInlSnd_seymour = Fintype.ofInjective (fun (x : { x₁ : Z × X₁ // f x₁.1 = Sum.inl x₁.2 }) => (↑x).1) ⋯

noncomputable instance instFintypeSubtypeProdEqSumFstInrSnd_seymour {X₁ X₂ Z : Type} [Fintype Z] {f : Z → X₁ ⊕ X₂} : Fintype { x₂ : Z × X₂ // f x₂.1 = Sum.inr x₂.2 }

Equations

• instFintypeSubtypeProdEqSumFstInrSnd_seymour = Fintype.ofInjective (fun (x : { x₂ : Z × X₂ // f x₂.1 = Sum.inr x₂.2 }) => (↑x).1) ⋯

theorem decomposeSum_card_eq {X₁ X₂ Z : Type} [Fintype Z] (f : Z → X₁ ⊕ X₂) : #{ x₁ : Z × X₁ // f x₁.1 = Sum.inl x₁.2 } + #{ x₂ : Z × X₂ // f x₂.1 = Sum.inr x₂.2 } = #Z

theorem Matrix.fromBlocks_isTotallyUnimodular {X₁ X₂ R : Type} [LinearOrderedCommRing R] [DecidableEq X₁] [DecidableEq X₂] {Y₁ Y₂ : Type} [DecidableEq Y₁] [DecidableEq Y₂] {A₁ : Matrix X₁ Y₁ R} {A₂ : Matrix X₂ Y₂ R} (hA₁ : A₁.IsTotallyUnimodular) (hA₂ : A₂.IsTotallyUnimodular) : (Matrix.fromBlocks A₁ 0 0 A₂).IsTotallyUnimodular

The block matrix that has two totally unimodular matrices along the diagonal and zeros elsewhere is totally unimodular.