Total Unimodularity

This file provides lemmas about total unimodularity that are not present in Mathlib.

@[simp]

theorem Matrix.empty_X_isTotallyUnimodular {X Y : Type} [IsEmpty X] {R : Type} [CommRing R] (A : Matrix X Y R) : A.IsTotallyUnimodular

@[simp]

theorem Matrix.empty_Y_isTotallyUnimodular {X Y : Type} [IsEmpty Y] {R : Type} [CommRing R] (A : Matrix X Y R) : A.IsTotallyUnimodular

@[simp]

theorem Matrix.overZ2_isTotallyUnimodular {X Y : Type} (A : Matrix X Y Z2) : A.IsTotallyUnimodular

Every matrix over Z2 is TU.

@[simp]

theorem Matrix.overZ3_isTotallyUnimodular {X Y : Type} (A : Matrix X Y Z3) : A.IsTotallyUnimodular

Every matrix over Z3 is TU.

theorem Matrix.IsTotallyUnimodular.det {X Y Z R : Type} [CommRing R] [DecidableEq Z] [Fintype Z] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) (f : Z → X) (g : Z → Y) : (A.submatrix f g).det ∈ Set.range SignType.cast

theorem Matrix.IsTotallyUnimodular.neg {X Y R : Type} [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) : (-A).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.det_eq_map_ratFloor_det {X : Type} [DecidableEq X] [Fintype X] {A : Matrix X X ℚ} (hA : A.IsTotallyUnimodular) : A.det = ↑(A.map Rat.floor).det

theorem Matrix.IsTotallyUnimodular.map_ratFloor {X Y : Type} {A : Matrix X Y ℚ} (hA : A.IsTotallyUnimodular) : (A.map Rat.floor).IsTotallyUnimodular

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

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

theorem Matrix.IsTotallyUnimodular.fromRows_comm {X₁ X₂ Y R : Type} [CommRing R] {A₁ : Matrix X₁ Y R} {A₂ : Matrix X₂ Y R} (hAA : (A₁ ⊟ A₂).IsTotallyUnimodular) : (A₂ ⊟ A₁).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.fromCols_comm {X Y₁ Y₂ R : Type} [CommRing R] {A₁ : Matrix X Y₁ R} {A₂ : Matrix X Y₂ R} (hAA : (A₁ ◫ A₂).IsTotallyUnimodular) : (A₂ ◫ A₁).IsTotallyUnimodular

theorem Matrix.replicateRow0_fromRows_isTotallyUnimodular_iff {X Y X' R : Type} [CommRing R] (A : Matrix X Y R) : (replicateRow X' 0 ⊟ A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

theorem Matrix.replicateCol0_fromCols_isTotallyUnimodular_iff {X Y Y' R : Type} [CommRing R] (A : Matrix X Y R) : (replicateCol Y' 0 ◫ A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.fromRows_zero {X Y R : Type} (X' : Type) [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) : (A ⊟ 0).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.zero_fromRows {X Y R : Type} (X' : Type) [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) : (0 ⊟ A).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.fromCols_zero {X Y R : Type} (Y' : Type) [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) : (A ◫ 0).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.zero_fromCols {X Y R : Type} (Y' : Type) [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) : (0 ◫ A).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.mul_rows {X Y R : Type} [DecidableEq X] [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) {q : X → R} (hq : ∀ (i : X), q i ∈ SignType.cast.range) : (of fun (i : X) (j : Y) => A i j * q i).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.mul_cols {X Y R : Type} [DecidableEq Y] [CommRing R] {A : Matrix X Y R} (hA : A.IsTotallyUnimodular) {q : Y → R} (hq : ∀ (j : Y), q j ∈ SignType.cast.range) : (of fun (i : X) (j : Y) => A i j * q j).IsTotallyUnimodular

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

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