English
Let K be a finite field with q elements, V a finite-dimensional vector space over K of dimension n, and k ≤ n. The set of all linear independent arrangements s: Fin k → V has cardinality ∏_{i=0}^{k-1} (q^n − q^i).
Русский
Пусть K — конечное поле с q элементами, V — векторное пространство над K размерности n, и k ≤ n. Множество всех линейно независимых наборов s: Fin k → V имеет размерность ∏_{i=0}^{k-1} (q^n − q^i).
LaTeX
$$Nat.card { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ i.val)$$
Lean4
/-- The cardinal of the set of linearly independent vectors over a finite-dimensional vector space
over a finite field. -/
theorem card_linearIndependent {k : ℕ} (hk : k ≤ n) :
Nat.card { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ i.val) :=
by
rw [Nat.card_eq_fintype_card]
induction k with
| zero =>
simp only [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero, card_ofSubsingleton,
Finset.univ_eq_empty, Finset.prod_empty]
| succ k
ih =>
have (s : { s : Fin k → V // LinearIndependent K s }) :
card ((Submodule.span K (Set.range (s : Fin k → V)))ᶜ : Set (V)) = (q) ^ n - (q) ^ k :=
by
rw [card_compl_set,
Module.card_eq_pow_finrank (K := K) (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
rw [Module.card_eq_pow_finrank (K := K)]
simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk), mul_comm,
Fin.prod_univ_succAbove _ (Fin.last k)]
