def Matrix.testTotallyUnimodular {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Bool

Formally verified algorithm for testing total unimodularity.

Equations

• A.testTotallyUnimodular = decide (∀ k ≤ m ⊓ n, ∀ (x : Fin k → Fin m) (y : Fin k → Fin n), (A.submatrix x y).det ∈ Set.range SignType.cast)

theorem Matrix.isTotallyUnimodular_of_aux_le {m n : ℕ} {A : Matrix (Fin m) (Fin n) ℚ} (hA : ∀ k ≤ m, ∀ (x : Fin k → Fin m) (y : Fin k → Fin n), (A.submatrix x y).det ∈ Set.range SignType.cast) : A.IsTotallyUnimodular

theorem Matrix.isTotallyUnimodular_of_testTotallyUnimodular {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : A.testTotallyUnimodular = true → A.IsTotallyUnimodular

theorem Matrix.testTotallyUnimodular_eq_isTotallyUnimodular {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : A.testTotallyUnimodular = true ↔ A.IsTotallyUnimodular

instance instDecidableIsTotallyUnimodularFinRat_seymour {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Decidable A.IsTotallyUnimodular

Equations

• instDecidableIsTotallyUnimodularFinRat_seymour A = decidable_of_iff (A.testTotallyUnimodular = true) ⋯

def Matrix.testTotallyUnimodularFaster {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Bool

Faster algorithm for testing total unimodularity but without formal guarantees.

Equations

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