Totally unimodular matrices

This file defines totally unimodular matrices and provides basic API for them.

Main definitions

• Matrix.IsTotallyUnimodular: a matrix is totally unimodular iff every square submatrix (not necessarily contiguous) has determinant 0 or 1 or -1.

Main results

• Matrix.isTotallyUnimodular_iff: a matrix is totally unimodular iff every square submatrix (possibly with repeated rows and/or repeated columns) has determinant 0 or 1 or -1.
• Matrix.IsTotallyUnimodular.apply: entry in a totally unimodular matrix is 0 or 1 or -1.

def Matrix.IsTotallyUnimodular {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) : Prop

Is the matrix A totally unimodular?

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.isTotallyUnimodular_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) : A.IsTotallyUnimodular ↔ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det = 0 ∨ (A.submatrix f g).det = 1 ∨ (A.submatrix f g).det = -1

theorem Matrix.IsTotallyUnimodular.apply {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyUnimodular) (i : m) (j : n) : A i j = 0 ∨ A i j = 1 ∨ A i j = -1

theorem Matrix.IsTotallyUnimodular.submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyUnimodular) {k : ℕ} (f : Fin k → m) (g : Fin k → n) : (A.submatrix f g).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyUnimodular) : A.transpose.IsTotallyUnimodular

theorem Matrix.transpose_isTotallyUnimodular_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) : A.transpose.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

theorem Matrix.mapEquiv_isTotallyUnimodular {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {X' : Type u_4} {Y' : Type u_5} (A : Matrix m n R) (eX : X' ≃ m) (eY : Y' ≃ n) : Matrix.IsTotallyUnimodular ((fun (x : m) => A x ∘ ⇑eY) ∘ ⇑eX) ↔ A.IsTotallyUnimodular

theorem Matrix.fromRows_row0_isTotallyUnimodular_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) {m' : Type u_4} : (A.fromRows (Matrix.row m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

theorem Matrix.fromColumns_col0_isTotallyUnimodular_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) {n' : Type u_4} : (A.fromColumns (Matrix.col n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular