IsTotallyUnimodular — Mathlib

English

A matrix is totally unimodular if every square submatrix has determinant 0, 1, or -1 (i.e., lies in the range of SignType.cast).

Русский

Матрица полностью унимодульная, если детерминант каждой квадратной подматрицы принадлежит {0, 1, -1}.

LaTeX

$$IsTotallyUnimodular(A) := ∀ k, ∀ f: Fin k → m, ∀ g: Fin k → n, f.Injective → g.Injective → det(A_{submatrix f g}) ∈ \\operatorname{range} \\operatorname{SignType.cast}$$

Lean4

/-- `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`. -/
def IsTotallyUnimodular (A : Matrix m n R) : Prop :=
  ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n, f.Injective → g.Injective → (A.submatrix f g).det ∈ Set.range SignType.cast

Похожие утверждения