feat(LinearAlgebra/Matrix/Determinant/TotallyUnimodular): iff_fintype (…

…#19366) add a lemma relating the definition of `Matrix.IsTotallyUnimodular` to `Fintype` rather than `Fin`. Co-authored-by: blizzard_inc <[email protected]>
leanprover-community · Nov 22, 2024 · be959a9 · be959a9
1 parent d380d2c
commit be959a9
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
@@ -54,6 +54,18 @@ lemma isTotallyUnimodular_iff (A : Matrix m n R) : A.IsTotallyUnimodular ↔
   · intro _ _ _ _ _
     apply hA
 
+lemma 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
+
 lemma IsTotallyUnimodular.apply {A : Matrix m n R} (hA : A.IsTotallyUnimodular)
     (i : m) (j : n) :
     A i j ∈ Set.range SignType.cast := by