# Erdős-Kaplansky theorem #

- `rank_dual_eq_card_dual_of_aleph0_le_rank`: The Erdős-Kaplansky Theorem which says that the dimension of an infinite-dimensional dual space over a division ring has dimension equal to its cardinality.

source
theorem max_aleph0_card_le_rank_fun_nat (K : Type u) [DivisionRing K] :
max Cardinal.aleph0 (Cardinal.mk K) ≤ Module.rank K (ℕ → K)

Key lemma towards the Erdős-Kaplansky theorem from https://mathoverflow.net/a/168624

source
theorem rank_fun_infinite {K : Type u} [DivisionRing K] {ι : Type v} [hι : Infinite ι] :
Module.rank K (ι → K) = Cardinal.mk (ι → K)
source
theorem rank_dual_eq_card_dual_of_aleph0_le_rank' {K : Type u} [DivisionRing K] {V : Type u_1} [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) :
Module.rank K ᵐᵒᵖ (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)

The Erdős-Kaplansky Theorem: the dual of an infinite-dimensional vector space over a division ring has dimension equal to its cardinality.

source
theorem rank_dual_eq_card_dual_of_aleph0_le_rank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) :
Module.rank K (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)

The Erdős-Kaplansky Theorem over a field.

source
theorem lift_rank_lt_rank_dual' {K : Type u} [DivisionRing K] {V : Type v} [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) :
Cardinal.lift.{u, v} (Module.rank K V) < Module.rank K ᵐᵒᵖ (V →ₗ[K] K)
source
theorem lift_rank_lt_rank_dual {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) :
Cardinal.lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)
source
theorem rank_lt_rank_dual' {K : Type u} [DivisionRing K] {V : Type u} [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) :
Module.rank K V < Module.rank K ᵐᵒᵖ (V →ₗ[K] K)
source
theorem rank_lt_rank_dual {K V : Type u} [Field K] [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) :
Module.rank K V < Module.rank K (V →ₗ[K] K)