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]
[Finite V]
{k : ℕ}
(hk : k ≤ Module.finrank K V)
:
The cardinal of the set of linearly independent vectors over a finite dimensional vector space over a finite field.
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.
Instances For
The cardinal of the general linear group over a finite field.