Theorems · Definition · linear algebra

Matrix.IsTotallyUnimodular

{m : Type u_1} → {n : Type u_3} → {R : Type u_5} → [CommRing R] → Matrix m n R → Prop

A.IsTotallyUnimodular means that every square submatrix of A (not necessarily contiguous) has determinant 0 or 1 or -1; that is, the determinant is in the range of SignType.cast.

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Cited by

22 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing