The order of GL₂ over a finite field

Mathlib's Matrix.card_GL_field gives |GL n 𝔽_q| = ∏ i, (qⁿ - qⁱ), which in size two reads (q² - 1)(q² - q). That form is a product of differences, and every index computation in GL₂ divides it by the order of a subgroup, so what is wanted is the factored form (q - 1)² · q · (q + 1), where the natural subtraction has already been carried out. It is recorded here in the two associations the two maximal tori call for: the split torus has order (q - 1)² and the non-split one q² - 1.

Main results

• TauCeti.natCard_GL_fin_two: |GL₂(𝔽_q)| = (q - 1)² · q(q + 1).
• TauCeti.natCard_GL_fin_two_eq_sq_sub_one_mul: |GL₂(𝔽_q)| = (q² - 1) · q(q - 1).

References

• Character theory roadmap, Layer 9, "The conjugacy classes (a build target)".

theorem TauCeti.natCard_GL_fin_two (F : Type u_1) [Field F] [Fintype F] : Nat.card (GL (Fin 2) F) = (Fintype.card F - 1) ^ 2 * (Fintype.card F * (Fintype.card F + 1))

The order of GL₂ over a finite field, in the factored form (q - 1)² · q(q + 1): the first factor is the order of the split torus and the second its index.

theorem TauCeti.natCard_GL_fin_two_eq_sq_sub_one_mul (F : Type u_1) [Field F] [Fintype F] : Nat.card (GL (Fin 2) F) = (Fintype.card F ^ 2 - 1) * (Fintype.card F * (Fintype.card F - 1))

The order of GL₂ over a finite field, in the factored form (q² - 1) · q(q - 1): the first factor is the order of the non-split torus and the second its index.