English
Under a hypothesis from Erdős–Kaplansky, the dual of an infinite-dimensional space has dimension equal to the cardinality of its dual space of linear functionals.
Русский
Согласно гипотезе Эрдеша–Каплански, двойственное пространства бесконечной размерности имеет размерность, равную мощности пространства линейных функционалов.
LaTeX
$$$\operatorname{rank}_{\mathrm{MulOpposite}(K)}(V \to_K K) = \#(V \to_K K)$, assuming $\aleph_0 \le \operatorname{Module.rank}_K(V)$$$
Lean4
/-- The **Erdős-Kaplansky Theorem**: the dual of an infinite-dimensional vector space
over a division ring has dimension equal to its cardinality. -/
theorem rank_dual_eq_card_dual_of_aleph0_le_rank' {V : Type*} [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.trans (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Kᵐᵒᵖ)
rw [e.rank_eq, e.toEquiv.cardinal_eq]
apply rank_fun_infinite
