English
Let V be a vector space over a field K with infinite dimension (at least countable). Then the dimension of its dual space V* = Hom_K(V,K) equals the cardinality of V*, i.e. dim_K(V*) = |V*|. In particular, the dual has a dimension that matches the size of the set of all linear functionals on V.
Русский
Пусть V — векторное пространство над полем K размерности не конечна (не менее ℵ0). Тогда размерность двойственного пространства V* = Hom_K(V,K) равна мощности множества V*, то есть dim_K(V*) = |V*|.
LaTeX
$$$\aleph_0 \le \operatorname{rank}_K V \Rightarrow \operatorname{rank}_K(V^*) = |V^*|,$$$
Lean4
/-- The **Erdős-Kaplansky Theorem** over a field. -/
theorem rank_dual_eq_card_dual_of_aleph0_le_rank {K V} [Field K] [AddCommGroup V] [Module K V]
(h : ℵ₀ ≤ Module.rank K V) : Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K) :=
by
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h
have e := (b.constr K (M' := K)).symm
rw [e.rank_eq, e.toEquiv.cardinal_eq]
apply rank_fun_infinite
