English
Let A be a matrix as above. Then A is totally unimodular if and only if for every finite index type ι (with Fintype and DecidableEq), for all f: ι → m and g: ι → n, the minor det(A.submatrix f g) lies in the range of SignType.cast (i.e., equals ±1 or 0).
Русский
Пусть A — матрица над кольцом R. Тогда A тотально унимодулярна тогда и только тогда, когда для каждого конечного индексового типа ι (с Fintype и DecidableEq) для любых отображений f: ι → m и g: ι → n детерминант подматрицы det(A_{f,g}) принадлежит образу SignType.cast (то есть равен −1, 0 или 1).
LaTeX
$$$A \\text{ is totally unimodular} \\iff \\forall \\iota\\ [Fintype(\\iota)] [DecidableEq(\\iota)], \\forall f: \\iota \\to m, \\forall g: \\iota \\to n, \\det(A_{f,g}) \\in \\operatorname{range}(\\operatorname{SignType.cast})$$$
Lean4
theorem isTotallyUnimodular_iff_fintype.{w} (A : Matrix m n R) :
A.IsTotallyUnimodular ↔
∀ (ι : Type w) [Fintype ι] [DecidableEq ι],
∀ f : ι → m, ∀ g : ι → n, (A.submatrix f g).det ∈ Set.range SignType.cast :=
by
rw [isTotallyUnimodular_iff]
constructor
· intro hA ι _ _ f g
specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA
· intro hA k f g
specialize hA (ULift (Fin k)) (f ∘ Equiv.ulift) (g ∘ Equiv.ulift)
rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA
