card_GL_field — Mathlib

English

The cardinality of GL_n(F) for a finite field F with q elements is ∏_{i=0}^{n-1} (q^n − q^i).

Русский

Кардинал GL_n(F) для конечного поля F с q элементами равен ∏_{i=0}^{n-1} (q^n − q^i).

LaTeX

$$Nat.card (GL (Fin n) F) = Finset.univ.prod (fun i => (q ^ n - q ^ i))$$

Lean4

/-- The cardinal of the general linear group over a finite field. -/
theorem card_GL_field : Nat.card (GL (Fin n) 𝔽) = ∏ i : (Fin n), (q ^ n - q ^ (i : ℕ)) :=
  by
  rw [Nat.card_congr (equiv_GL_linearindependent n), card_linearIndependent, Module.finrank_fintype_fun_eq_card,
    Fintype.card_fin]
  simp only [Module.finrank_fintype_fun_eq_card, Fintype.card_fin, le_refl]

Похожие утверждения