From be959a9ade921f874584eb5761e7c4f6c82f6651 Mon Sep 17 00:00:00 2001 From: blizzard_inc Date: Fri, 22 Nov 2024 13:33:56 +0000 Subject: [PATCH] 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 --- .../Matrix/Determinant/TotallyUnimodular.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean index cd7b6cae09bfd..03da13b5d1757 100644 --- 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