Total Unimodularity #
This file provides lemmas about total unimodularity that are not present in Mathlib.
theorem
Matrix.IsTotallyUnimodular.det
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{R : Type u_4}
[CommRing R]
[DecidableEq Z]
[Fintype Z]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
(f : Z → X)
(g : Z → Y)
:
theorem
Matrix.IsTotallyUnimodular.neg
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
[CommRing R]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
:
theorem
Matrix.IsTotallyUnimodular.det_eq_map_ratFloor_det
{X : Type u_1}
[DecidableEq X]
[Fintype X]
{A : Matrix X X ℚ}
(hA : A.IsTotallyUnimodular)
:
theorem
Matrix.IsTotallyUnimodular.map_ratFloor
{X : Type u_1}
{Y : Type u_2}
{A : Matrix X Y ℚ}
(hA : A.IsTotallyUnimodular)
:
theorem
Matrix.IsTotallyUnimodular.comp_rows
{X : Type u_1}
{Y : Type u_2}
{X' : Type u_3}
{R : Type u_4}
[CommRing R]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
(e : X' → X)
:
IsTotallyUnimodular (A ∘ e)
theorem
Matrix.IsTotallyUnimodular.comp_cols
{X : Type u_1}
{Y : Type u_2}
{Y' : Type u_3}
{R : Type u_4}
[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₁ : Type u_1}
{X₂ : Type u_2}
{Y : Type u_3}
{R : Type u_4}
[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 : Type u_1}
{Y₁ : Type u_2}
{Y₂ : Type u_3}
{R : Type u_4}
[CommRing R]
{A₁ : Matrix X Y₁ R}
{A₂ : Matrix X Y₂ R}
(hAA : (A₁ ◫ A₂).IsTotallyUnimodular)
:
(A₂ ◫ A₁).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.fromRows_zero
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
(X' : Type u_4)
[CommRing R]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
:
(A ⊟ 0).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.zero_fromRows
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
(X' : Type u_4)
[CommRing R]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
:
(0 ⊟ A).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.fromCols_zero
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
(Y' : Type u_4)
[CommRing R]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
:
(A ◫ 0).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.zero_fromCols
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
(Y' : Type u_4)
[CommRing R]
{A : Matrix X Y R}
(hA : A.IsTotallyUnimodular)
:
(0 ◫ A).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.mul_rows
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
[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 : Type u_1}
{Y : Type u_2}
{R : Type u_3}
[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₁ : Type u_1}
{X₂ : Type u_2}
{Y₁ : Type u_3}
{Y₂ : Type u_4}
{R : Type u_5}
[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.