# Dimension of vector spaces #

In this file we provide results about Module.rank and FiniteDimensional.finrank of vector spaces over division rings.

## Main statements #

For vector spaces (i.e. modules over a field), we have

• rank_quotient_add_rank_of_divisionRing: if V₁ is a submodule of V, then Module.rank (V/V₁) + Module.rank V₁ = Module.rank V.
• rank_range_add_rank_ker: the rank-nullity 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.
theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 {K : Type u} {V : Type v} [] [] [Module K V] (h : ) :
().Finite

If a vector space has a finite dimension, the index set of Basis.ofVectorSpace is finite.

theorem rank_quotient_add_rank_of_divisionRing {K : Type u} {V : Type v} [] [] [Module K V] (p : ) :
Module.rank K (V p) + Module.rank K p =

Also see rank_quotient_add_rank.

instance DivisionRing.hasRankNullity {K : Type u} [] :
Equations
• =
theorem rank_add_rank_split {K : Type u} {V : Type v} {V₁ : Type v} {V₂ : Type v} {V₃ : Type v} [] [] [Module K V] [] [Module K V₁] [] [Module K V₂] [] [Module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂) (ce : V₁ →ₗ[K] V₃) (hde : ) (hgd : ) (eq : db ∘ₗ cd = eb ∘ₗ ce) (eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e∃ (c : V₁), cd c = d ce c = e) :
+ Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

This is mostly an auxiliary lemma for Submodule.rank_sup_add_rank_inf_eq.

theorem linearIndependent_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_2} [] {b : ιV} (spans : ) (card_eq : ) :
theorem linearIndependent_iff_card_eq_finrank_span {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_2} [] {b : ιV} :

A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.

theorem linearIndependent_iff_card_le_finrank_span {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_2} [] {b : ιV} :
noncomputable def basisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_2} [] (b : ιV) (le_span : ) (card_eq : ) :
Basis ι K V

A family of finrank K V vectors forms a basis if they span the whole space.

Equations
Instances For
@[simp]
theorem coe_basisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_2} [] (b : ιV) (le_span : ) (card_eq : ) :
(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b
@[simp]
theorem finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [] [] [Module K V] {s : } (le_span : ) (card_eq : s.card = ) :
∀ (a : V), (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = .repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ) a)
noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {s : } (le_span : ) (card_eq : s.card = ) :
Basis { x : V // x s } K V

A finset of finrank K V vectors forms a basis if they span the whole space.

Equations
Instances For
@[simp]
theorem setBasisOfTopLeSpanOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [] [] [Module K V] {s : Set V} [Fintype s] (le_span : ) (card_eq : s.toFinset.card = ) :
∀ (a : V), (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = .repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ) a)
noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {s : Set V} [Fintype s] (le_span : ) (card_eq : s.toFinset.card = ) :
Basis (s) K V

A set of finrank K V vectors forms a basis if they span the whole space.

Equations
Instances For
theorem max_aleph0_card_le_rank_fun_nat (K : Type u) [] :
Module.rank K (K)

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

theorem rank_fun_infinite {K : Type u} [] {ι : Type v} [hι : ] :
Module.rank K (ιK) = Cardinal.mk (ιK)
theorem rank_dual_eq_card_dual_of_aleph0_le_rank' {K : Type u} [] {V : Type u_2} [] [Module K V] (h : ) :

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 {K : Type u_2} {V : Type u_3} [] [] [Module K V] (h : ) :

The Erdős-Kaplansky Theorem over a field.

theorem lift_rank_lt_rank_dual' {K : Type u} [] {V : Type v} [] [Module K V] (h : ) :
theorem lift_rank_lt_rank_dual {K : Type u} {V : Type v} [] [] [Module K V] (h : ) :
theorem rank_lt_rank_dual' {K : Type u} [] {V : Type u} [] [Module K V] (h : ) :
theorem rank_lt_rank_dual {K : Type u} {V : Type u} [] [] [Module K V] (h : ) :