English
Let A be an m × n matrix over a commutative ring R. Then A is totally unimodular if and only if every square submatrix has determinant lying in {−1, 0, 1} (i.e., in the image of the sign-cast).
Русский
Пусть A — матрица размера m × n над коммутативным кольцом R. Тогда A тотально унимодулярна тогда и только тогда, когда детерминант каждой квадратной подматрицы принадлежит множеству {−1, 0, 1}.
LaTeX
$$$A \\text{ is totally unimodular} \\iff \\forall k \\in \\mathbb{N}, \\forall f: \\mathrm{Fin}(k) \\to m, \\forall g: \\mathrm{Fin}(k) \\to n, \\det(A_{f,g}) \\in \\operatorname{range}(\\operatorname{SignType.cast})$$$
Lean4
theorem isTotallyUnimodular_iff (A : Matrix m n R) :
A.IsTotallyUnimodular ↔
∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n, (A.submatrix f g).det ∈ Set.range SignType.cast :=
by
constructor <;> intro hA
· intro k f g
by_cases hfg : f.Injective ∧ g.Injective
· exact hA k f g hfg.1 hfg.2
· use 0
rw [SignType.coe_zero, eq_comm]
simp_rw [not_and_or, Function.not_injective_iff] at hfg
obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg
· rw [← det_transpose, transpose_submatrix]
apply det_zero_of_column_eq hij.symm
simp [hfij]
· apply det_zero_of_column_eq hij
simp [hgij]
· intro _ _ _ _ _
apply hA
