Cardinal of the general linear group over finite rings

This file computes the cardinal of the general linear group over finite rings.

Main statements

• card_linearIndependent gives the cardinal of the set of linearly independent vectors over a finite-dimensional vector space over a finite field.
• Matrix.card_GL_field gives the cardinal of the general linear group over a finite field.

theorem card_linearIndependent {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [Fintype K] [Finite V] {k : ℕ} (hk : k ≤ Module.finrank K V) : Nat.card { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (Fintype.card K ^ Module.finrank K V - Fintype.card K ^ ↑i)

The cardinal of the set of linearly independent vectors over a finite-dimensional vector space over a finite field.

theorem Matrix.card_SL_mul_card_units {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {R : Type u_2} [CommRing R] : Nat.card (SpecialLinearGroup n R) * Nat.card Rˣ = Nat.card (GL n R)

The cardinal of the special linear group times the cardinal of the unit group is the cardinal of the general linear group.

theorem Matrix.card_SL {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {R : Type u_2} [CommRing R] [Finite Rˣ] : Nat.card (SpecialLinearGroup n R) = Nat.card (GL n R) / Nat.card Rˣ

The cardinal of the special linear group over a commutative ring with finitely many units.

theorem Matrix.card_matrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [Finite m] [Finite n] : Nat.card (Matrix m n α) = Nat.card α ^ (Nat.card n * Nat.card m)

The cardinal of a matrix.

theorem Matrix.enatCard_matrix {m : Type u_1} {n : Type u_2} {α : Type u_3} : ENat.card (Matrix m n α) = ENat.card α ^ (ENat.card n * ENat.card m)

noncomputable def Matrix.equiv_GL_linearindependent {𝔽 : Type u_1} [Field 𝔽] [Fintype 𝔽] (n : ℕ) : GL (Fin n) 𝔽 ≃ { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }

Equivalence between GL n F and n vectors of length n that are linearly independent. Given by sending a matrix to its columns.

Equations

• One or more equations did not get rendered due to their size.

theorem Matrix.card_GL_field {𝔽 : Type u_1} [Field 𝔽] [Fintype 𝔽] (n : ℕ) : Nat.card (GL (Fin n) 𝔽) = ∏ i : Fin n, (Fintype.card 𝔽 ^ n - Fintype.card 𝔽 ^ ↑i)

The cardinal of the general linear group over a finite field.

theorem Matrix.card_SL_field {𝔽 : Type u_1} [Field 𝔽] [Fintype 𝔽] (n : ℕ) [NeZero n] : Nat.card (SpecialLinearGroup (Fin n) 𝔽) = (∏ i : Fin n, (Fintype.card 𝔽 ^ n - Fintype.card 𝔽 ^ ↑i)) / (Fintype.card 𝔽 - 1)

The cardinal of the special linear group over a finite field.