Theorems · Theorem · group theory

card_linearIndependent

∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : Fintype K] [Finite V] {k : ℕ},
  k ≤ Module.finrank K V →
    Nat.card { s // LinearIndependent K s } = ∏ i, (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.

Defined in

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Cited by

1 results in Mathlib

Foundations

Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleFintypeFinite