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_linearInependent 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] [Fintype V] {k : ℕ} (hk : k ≤ FiniteDimensional.finrank K V) : Nat.card { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (Fintype.card K ^ FiniteDimensional.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.

noncomputable def Matrix.equiv_GL_linearindependent {𝔽 : Type u_1} [Field 𝔽] (n : ℕ) (hn : 0 < 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 coloumns.

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.