feat: SpecialLinearGroup n R is finite when R is (#17629)

From GrowthInGroups
leanprover-community · Oct 11, 2024 · fe48a46 · fe48a46
1 parent 3390e40
commit fe48a46
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
@@ -124,6 +124,9 @@ instance : Pow (SpecialLinearGroup n R) ℕ where
 instance : Inhabited (SpecialLinearGroup n R) :=
   ⟨1⟩
 
+instance [Fintype R] [DecidableEq R] : Fintype (SpecialLinearGroup n R) := Subtype.fintype _
+instance [Finite R] : Finite (SpecialLinearGroup n R) := Subtype.finite
+
 /-- The transpose of a matrix in `SL(n, R)` -/
 def transpose (A : SpecialLinearGroup n R) : SpecialLinearGroup n R :=
   ⟨A.1.transpose, A.1.det_transpose ▸ A.2⟩