English
If K and V are as above with V finite over K and free, then the cardinality of V equals the cardinality of K raised to the rank of V: |V| = |K|^{rank_K V}.
Русский
Пусть K и V удовлетворяют условиям, что V конечно-размерно над K и свободно. Тогда кардинал множества V равен кардиналу поля K в степени размерности V: |V| = |K|^{rank_K V}.
LaTeX
$$$|V| = |K|^{\operatorname{rank} K V}$$$
Lean4
theorem lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank [Module.Free K V] [Module.Finite K V] :
lift.{u} #V = lift.{v} #K ^ lift.{u} (Module.rank K V) :=
by
haveI := nontrivial_of_invariantBasisNumber K
obtain ⟨s, hs⟩ :=
Module.Free.exists_basis (R := K) (M := V)
-- `Module.Finite.finite_basis` is in a much later file, so we copy its proof to here
haveI : Finite s := by
obtain ⟨t, ht⟩ := ‹Module.Finite K V›
exact basis_finite_of_finite_spans t.finite_toSet ht hs
have := lift_mk_eq'.2 ⟨hs.repr.toEquiv⟩
rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift, lift_lift,
lift_umax] at this
