From b6fe43dfe490d6749abab69bd8135fa836cb6017 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 21 Mar 2024 14:51:10 +0000
Subject: [PATCH] chore(LinearAlgebra): fix Fintype/Finite assumptions (#11565)

.. in `equivOfPiLEquivPi`, `coePiBasisFun.toMatrix_eq_transpose`, `vecMul_surjective_iff_exists_left_inverse`, and `mulVec_surjective_iff_exists_right_inverse`
---
 Mathlib/LinearAlgebra/Determinant.lean        |  7 +++-
 Mathlib/LinearAlgebra/Matrix/Basis.lean       |  2 +-
 .../Matrix/NonsingularInverse.lean            | 39 +++++++++++++------
 3 files changed, 34 insertions(+), 14 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean
index 172877c760af8..ccfa638e3b585 100644
--- a/Mathlib/LinearAlgebra/Determinant.lean
+++ b/Mathlib/LinearAlgebra/Determinant.lean
@@ -55,15 +55,18 @@ variable (e : Basis ι R M)
 section Conjugate
 
 variable {A : Type*} [CommRing A]
-variable {m n : Type*} [Fintype m] [Fintype n]
+variable {m n : Type*}
 
 /-- If `R^m` and `R^n` are linearly equivalent, then `m` and `n` are also equivalent. -/
-def equivOfPiLEquivPi {R : Type*} [CommRing R] [Nontrivial R] (e : (m → R) ≃ₗ[R] n → R) : m ≃ n :=
+def equivOfPiLEquivPi {R : Type*} [Finite m] [Finite n] [CommRing R] [Nontrivial R]
+    (e : (m → R) ≃ₗ[R] n → R) : m ≃ n :=
   Basis.indexEquiv (Basis.ofEquivFun e.symm) (Pi.basisFun _ _)
 #align equiv_of_pi_lequiv_pi equivOfPiLEquivPi
 
 namespace Matrix
 
+variable [Fintype m] [Fintype n]
+
 /-- If `M` and `M'` are each other's inverse matrices, they are square matrices up to
 equivalence of types. -/
 def indexEquivOfInv [Nontrivial A] [DecidableEq m] [DecidableEq n] {M : Matrix m n A}
diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean
index 4a9bf8bbbc762..eb2e9a38facad 100644
--- a/Mathlib/LinearAlgebra/Matrix/Basis.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Basis.lean
@@ -72,7 +72,7 @@ theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M)
 #align basis.to_matrix_eq_to_matrix_constr Basis.toMatrix_eq_toMatrix_constr
 
 -- TODO (maybe) Adjust the definition of `Basis.toMatrix` to eliminate the transpose.
-theorem coePiBasisFun.toMatrix_eq_transpose [Fintype ι] :
+theorem coePiBasisFun.toMatrix_eq_transpose [Finite ι] :
     ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose := by
   ext M i j
   rfl
diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
index 7b7fb53579a2b..7a94a6c4c1017 100644
--- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
+++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
@@ -193,6 +193,8 @@ theorem det_ne_zero_of_right_inverse [Nontrivial α] (h : A * B = 1) : A.det ≠
 
 end Invertible
 
+section Inv
+
 variable [Fintype n] [DecidableEq n] [CommRing α]
 variable (A : Matrix n n α) (B : Matrix n n α)
 
@@ -352,13 +354,15 @@ lemma mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A * x =
 lemma mul_left_inj_of_invertible [Invertible A] {x y : Matrix m n α} : x * A = y * A ↔ x = y :=
   (mul_left_injective_of_invertible A).eq_iff
 
+end Inv
+
 section InjectiveMul
-variable [Fintype m] [DecidableEq m]
+variable [Fintype n] [Fintype m] [DecidableEq m] [CommRing α]
 variable [Fintype l] [DecidableEq l]
 
 lemma mul_left_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
-    Function.Injective (fun x : Matrix l m α => x * A) :=
-  fun _ _ g => by simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g
+    Function.Injective (fun x : Matrix l m α => x * A) := fun _ _ g => by
+  simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g
 
 lemma mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
     Function.Injective (fun x : Matrix m l α => B * x) :=
@@ -368,29 +372,39 @@ end InjectiveMul
 
 section vecMul
 
-variable [Fintype m] [DecidableEq m] {K R : Type*} [Field K]
+variable [DecidableEq m] [DecidableEq n]
+
+section Semiring
 
-theorem vecMul_surjective_iff_exists_left_inverse [Semiring R] {A : Matrix m n R} :
+variable {R : Type*} [Semiring R]
+
+theorem vecMul_surjective_iff_exists_left_inverse [Fintype m] [Finite n] {A : Matrix m n R} :
     Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by
+  cases nonempty_fintype n
   refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
   choose rows hrows using (h <| Pi.single · 1)
   refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
   rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]
   rfl
 
-theorem mulVec_surjective_iff_exists_right_inverse [Semiring R] {A : Matrix m n R} :
+theorem mulVec_surjective_iff_exists_right_inverse [Finite m] [Fintype n] {A : Matrix m n R} :
     Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by
+  cases nonempty_fintype m
   refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
   choose cols hcols using (h <| Pi.single · 1)
   refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
   rw [one_eq_pi_single, Pi.single_comm, ← hcols j]
   rfl
 
-theorem vecMul_surjective_iff_isUnit {A : Matrix m m α} :
+end Semiring
+
+variable {R K : Type*} [CommRing R] [Field K] [Fintype m]
+
+theorem vecMul_surjective_iff_isUnit {A : Matrix m m R} :
     Function.Surjective A.vecMul ↔ IsUnit A := by
   rw [vecMul_surjective_iff_exists_left_inverse, exists_left_inverse_iff_isUnit]
 
-theorem mulVec_surjective_iff_isUnit {A : Matrix m m α} :
+theorem mulVec_surjective_iff_isUnit {A : Matrix m m R} :
     Function.Surjective A.mulVec ↔ IsUnit A := by
   rw [mulVec_surjective_iff_exists_right_inverse, exists_right_inverse_iff_isUnit]
 
@@ -420,11 +434,11 @@ theorem linearIndependent_cols_iff_isUnit {A : Matrix m m K} :
   rw [← transpose_transpose A, isUnit_transpose, linearIndependent_rows_iff_isUnit,
     transpose_transpose]
 
-theorem vecMul_surjective_of_invertible (A : Matrix m m α) [Invertible A] :
+theorem vecMul_surjective_of_invertible (A : Matrix m m R) [Invertible A] :
     Function.Surjective A.vecMul :=
   vecMul_surjective_iff_isUnit.2 <| isUnit_of_invertible A
 
-theorem mulVec_surjective_of_invertible (A : Matrix m m α) [Invertible A] :
+theorem mulVec_surjective_of_invertible (A : Matrix m m R) [Invertible A] :
     Function.Surjective A.mulVec :=
   mulVec_surjective_iff_isUnit.2 <| isUnit_of_invertible A
 
@@ -446,6 +460,9 @@ theorem linearIndependent_cols_of_invertible (A : Matrix m m K) [Invertible A] :
 
 end vecMul
 
+variable [Fintype n] [DecidableEq n] [CommRing α]
+variable (A : Matrix n n α) (B : Matrix n n α)
+
 theorem nonsing_inv_cancel_or_zero : A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0 := by
   by_cases h : IsUnit A.det
   · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩
@@ -760,7 +777,7 @@ end Submatrix
 
 section Det
 
-variable [Fintype m] [DecidableEq m]
+variable [Fintype m] [DecidableEq m] [CommRing α]
 
 /-- A variant of `Matrix.det_units_conj`. -/
 theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M * N * M⁻¹) = det N :=