[Merged by Bors] - feat: Cardinal of GLn with coefficients in a finite field

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -197,6 +197,7 @@ theorem hom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : CliffordAlgebra Q
 #align clifford_algebra.hom_ext CliffordAlgebra.hom_ext
 
 -- This proof closely follows `TensorAlgebra.induction`
+attribute [-instance] IntermediateField.module' normalClosure.algebra in
 /-- If `C` holds for the `algebraMap` of `r : R` into `CliffordAlgebra Q`, the `ι` of `x : M`,
 and is preserved under addition and muliplication, then it holds for all of `CliffordAlgebra Q`.
 

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

@@ -7,6 +7,8 @@ import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 import Mathlib.Algebra.Ring.Subring.Units
+import Mathlib.FieldTheory.Finite.Basic
+import Mathlib.Data.Matrix.Rank
 
 #align_import linear_algebra.matrix.general_linear_group from "leanprover-community/mathlib"@"2705404e701abc6b3127da906f40bae062a169c9"
 
@@ -329,4 +331,92 @@ def planeConformalMatrix {R} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) :
 -/
 end Examples
 
+section cardinal
+
+variable (n : ℕ) {𝔽 : Type*} [Field 𝔽] [Fintype 𝔽]
+
+local notation "q" => Fintype.card 𝔽
+
+noncomputable instance {k : ℕ} :
+    Fintype ({ s : Fin k → (Fin n → 𝔽) // LinearIndependent 𝔽 s}) :=
+  Fintype.ofFinite _
+
+noncomputable instance {k : ℕ} {s : { s : Fin k → Fin n → 𝔽 // LinearIndependent 𝔽 s }} :
+    Fintype (Submodule.span 𝔽 (Set.range (s : Fin k → Fin n → 𝔽)) : Set (Fin n → 𝔽)) :=
+  Fintype.ofFinite _
+
+noncomputable instance {k : ℕ} {s : { s : Fin k → Fin n → 𝔽 // LinearIndependent 𝔽 s }} :
+    Fintype ((Submodule.span 𝔽 (Set.range (s : Fin k → Fin n → 𝔽)))ᶜ : Set (Fin n → 𝔽)) :=
+  Fintype.ofFinite _
+
+lemma complement_card {k : ℕ} (s : { s : Fin k → Fin n → 𝔽 // LinearIndependent 𝔽 s }):
+    Fintype.card ((Submodule.span 𝔽 (Set.range (s : Fin k → Fin n → 𝔽)))ᶜ : Set (Fin n → 𝔽)) =
+      (q) ^ n - (q) ^ k := by
+  simp only [Fintype.card_compl_set, Fintype.card_pi, Finset.prod_const, Finset.card_univ,
+    Fintype.card_fin, SetLike.coe_sort_coe,
+    card_eq_pow_finrank (K := 𝔽) (V := Submodule.span 𝔽 (Set.range (s : Fin k → Fin n → 𝔽))),
+    finrank_span_eq_card s.property]
+
+/-- Equivalence between `k + 1` vectors of length `n` and `k` vectors of length `n` along with a
+vector in the complement of their span.
+-/
+def inductiveStepEquiv {k : ℕ} :
+    { s : Fin (k + 1) → Fin n → 𝔽 // LinearIndependent 𝔽 s } ≃
+      Σ s : { s : Fin k → Fin n → 𝔽 // LinearIndependent 𝔽 s },
+        ((Submodule.span 𝔽 (Set.range (s : Fin k → Fin n → 𝔽)))ᶜ : Set (Fin n → 𝔽)) where
+  toFun s := by
+    refine ⟨⟨Fin.tail s.val, (linearIndependent_fin_succ.mp s.property).left⟩,
+      ⟨s.val 0, (linearIndependent_fin_succ.mp s.property).right⟩⟩
+  invFun s := by
+    refine ⟨Fin.cons s.2.val s.1.val, linearIndependent_fin_cons.mpr ⟨s.1.property, s.2.property⟩⟩
+  left_inv _ := by simp only [Fin.cons_self_tail, Subtype.coe_eta]
+  right_inv := fun ⟨_, _⟩ => by simp only [Fin.cons_zero, Subtype.coe_eta, Sigma.mk.inj_iff,
+    Fin.tail_cons, heq_eq_eq, and_self]
+
+lemma card_LinearInependent_subtype {k : ℕ} (hk : k ≤ n) :
+    Fintype.card { s : Fin k → (Fin n → 𝔽) // LinearIndependent 𝔽 s } =
+      ∏ i : Fin k, ((q) ^ n - (q) ^ i.val) := by
+  induction' k with k ih
+  · simp only [Nat.zero_eq, LinearIndependent, Finsupp.total_fin_zero, LinearMap.ker_zero,
+    Fintype.card_ofSubsingleton, Finset.univ_eq_empty, Finset.prod_empty]
+  · simp only [Fintype.card_congr (inductiveStepEquiv n), Fintype.card_sigma, complement_card n,
+    Finset.sum_const, Finset.card_univ, ih (Nat.le_of_succ_le hk), smul_eq_mul, mul_comm,
+    Fin.prod_univ_succAbove _ k, Fin.natCast_eq_last, Fin.val_last, Fin.succAbove_last,
+    Fin.coe_castSucc]
+
+/-- Equivalence between `GL n F` and `n` vectors of length `n` that are linearly independent. Given
+by sending a matrix to its coloumns. -/
+noncomputable def equiv_GL_linearindependent {F : Type*} [Field F] (hn : 0 < n) :
+    GL (Fin n) F ≃ { s : Fin n → (Fin n → F) // LinearIndependent F s } where
+  toFun M := ⟨transpose M, by
+    apply linearIndependent_iff_card_eq_finrank_span.2
+    rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]⟩
+  invFun M := by
+    apply GeneralLinearGroup.mk'' (transpose (M.1))
+    rw [show M.1ᵀ = Basis.toMatrix (Pi.basisFun F (Fin n)) (transpose (M.1)ᵀ) by rfl,
+      transpose_transpose]
+    have : Nonempty (Fin n) := Fin.pos_iff_nonempty.1 hn
+    have hdim : Fintype.card (Fin n) = FiniteDimensional.finrank F (Fin n → F) := by
+      simp only [Fintype.card_fin, FiniteDimensional.finrank_fintype_fun_eq_card]
+    let b := basisOfLinearIndependentOfCardEqFinrank M.2 hdim
+    rw [show M = ⇑b by simp only [b, coe_basisOfLinearIndependentOfCardEqFinrank]]
+    have : Invertible ((Pi.basisFun F (Fin n)).toMatrix ⇑b) :=
+      (Pi.basisFun F (Fin n)).invertibleToMatrix b
+    exact isUnit_det_of_invertible _
+  left_inv := fun x ↦ Units.ext (ext fun i j ↦ rfl)
+  right_inv := by exact congrFun rfl
+
+noncomputable instance : Fintype (GL (Fin n) 𝔽) := by
+    exact Fintype.ofFinite (GL (Fin n) 𝔽)
+
+theorem card_GL : Fintype.card (GL (Fin n) 𝔽) = ∏ i : (Fin n), (q ^ (n) - q ^ ( i : ℕ )) := by
+  by_cases hn : n = 0
+  · rw [hn]
+    simp only [Fintype.card_unique, Finset.univ_eq_empty, mul_zero, pow_zero,
+    Finset.prod_empty]
+  · rw [Fintype.card_congr (equiv_GL_linearindependent n (Nat.pos_of_ne_zero hn))]
+    exact card_LinearInependent_subtype _ (Nat.le_refl n)
+
+end cardinal
+
 end Matrix