# mathlibdocumentation

linear_algebra.dimension

# Dimension of modules and vector spaces

## Main definitions

• The dimension of a vector space is defined as vector_space.dim : cardinal.

## Main statements

• mk_eq_mk_of_basis: the dimension theorem, any two bases of the same vector space have the same cardinality.
• dim_quotient_add_dim: if V₁ is a submodule of V, then dim (V/V₁) + dim V₁ = dim V.
• dim_range_add_dim_ker: the rank-nullity theorem.

## Implementation notes

Many theorems in this file are not universe-generic when they relate dimensions in different universes. They should be as general as they can be without inserting lifts. The types V, V', ... all live in different universes, and V₁, V₂, ... all live in the same universe.

def vector_space.dim (K : Type u) (V : Type v) [field K] [ V] :

the dimension of a vector space, defined as a term of type cardinal

Equations
theorem is_basis.le_span {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} {J : set V} :
v = # (set.range v) # J

theorem mk_eq_mk_of_basis {K : Type u} {V : Type v} {ι : Type w} {ι' : Type w'} [field K] [ V] {v : ι → V} {v' : ι' → V} :
v v'(# ι).lift = (# ι').lift

dimension theorem

theorem mk_eq_mk_of_basis' {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {ι' : Type w} {v : ι → V} {v' : ι' → V} :
v v'# ι = # ι'

theorem is_basis.mk_eq_dim'' {K : Type u} {V : Type v} [field K] [ V] {ι : Type v} {v : ι → V} :
v# ι =

theorem is_basis.mk_range_eq_dim {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} :
v# (set.range v) =

theorem is_basis.mk_eq_dim {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} :
v(# ι).lift = V).lift

theorem is_basis.mk_eq_dim' {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} :
v(# ι).lift = V).lift

theorem dim_le {K : Type u} {V : Type v} [field K] [ V] {n : } :
(∀ (s : finset V), (λ (i : s), i)s.card n) n

theorem linear_equiv.dim_eq {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] :
(V ≃ₗ[K] V₁) = V₁

Two linearly equivalent vector spaces have the same dimension.

@[simp]
theorem dim_bot {K : Type u} {V : Type v} [field K] [ V] :

@[simp]
theorem dim_top {K : Type u} {V : Type v} [field K] [ V] :

theorem dim_of_field (K : Type u_1) [field K] :
= 1

theorem dim_span {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} :
(set.range v)) = # (set.range v)

theorem dim_span_set {K : Type u} {V : Type v} [field K] [ V] {s : set V} :
(λ (x : s), x) s) = # s

theorem cardinal_lift_le_dim_of_linear_independent {K : Type u} {V : Type v} [field K] [ V] {ι : Type w} {v : ι → V} :
(# ι).lift V).lift

theorem cardinal_le_dim_of_linear_independent {K : Type u} {V : Type v} [field K] [ V] {ι : Type v} {v : ι → V} :
# ι

theorem cardinal_le_dim_of_linear_independent' {K : Type u} {V : Type v} [field K] [ V] {s : set V} :
(λ (x : s), x)# s

theorem dim_span_le {K : Type u} {V : Type v} [field K] [ V] (s : set V) :
s) # s

theorem dim_span_of_finset {K : Type u} {V : Type v} [field K] [ V] (s : finset V) :

theorem dim_prod {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] :
(V × V₁) = + V₁

theorem dim_quotient_add_dim {K : Type u} {V : Type v} [field K] [ V] (p : V) :
=

theorem dim_quotient_le {K : Type u} {V : Type v} [field K] [ V] (p : V) :

theorem dim_range_add_dim_ker {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :
(f.range) + (f.ker) =

rank-nullity theorem

theorem dim_range_le {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :

theorem dim_map_le {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) (p : V) :
p)

theorem dim_range_of_surjective {K : Type u} {V : Type v} {V' : Type v'} [field K] [ V] [add_comm_group V'] [ V'] (f : V →ₗ[K] V') :
(f.range) = V'

theorem dim_eq_of_surjective {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :
= V₁ + (f.ker)

theorem dim_le_of_surjective {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :
V₁

theorem dim_eq_of_injective {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :
= (f.range)

theorem dim_submodule_le {K : Type u} {V : Type v} [field K] [ V] (s : V) :

theorem dim_le_of_injective {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :
V₁

theorem dim_le_of_submodule {K : Type u} {V : Type v} [field K] [ V] (s t : V) :
s t

theorem linear_independent_le_dim {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} :
(# ι).lift V).lift

theorem linear_independent_le_dim' {K : Type u} {V : Type v} {ι : Type w} [field K] [ V] {v : ι → V} :
(# ι).lift V).lift

theorem dim_add_dim_split {K : Type u} {V V₁ V₂ V₃ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] [add_comm_group V₂] [ V₂] [add_comm_group V₃] [ V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂) (ce : V₁ →ₗ[K] V₃) :
db.range eb.rangecd.ker = db.comp cd = eb.comp ce(∀ (d : V₂) (e : V₃), db d = eb e(∃ (c : V₁), cd c = d ce c = e)) + V₁ = V₂ + V₃

This is mostly an auxiliary lemma for dim_sup_add_dim_inf_eq.

theorem dim_sup_add_dim_inf_eq {K : Type u} {V : Type v} [field K] [ V] (s t : V) :
(s t) + (s t) =

theorem dim_add_le_dim_add_dim {K : Type u} {V : Type v} [field K] [ V] (s t : V) :
(s t)

theorem dim_pi {K : Type u} {η : Type u₁'} {φ : η → Type u_1} [field K] [fintype η] [Π (i : η), add_comm_group (φ i)] [Π (i : η), (φ i)] :
(Π (i : η), φ i) = cardinal.sum (λ (i : η), (φ i))

theorem dim_fun {K : Type u} [field K] {V η : Type u} [fintype η] [ V] :
(η → V) = ((fintype.card η)) *

theorem dim_fun_eq_lift_mul {K : Type u} {V : Type v} {η : Type u₁'} [field K] [ V] [fintype η] :
(η → V) = ((fintype.card η)) * V).lift

theorem dim_fun' {K : Type u} {η : Type u₁'} [field K] [fintype η] :
(η → K) = (fintype.card η)

theorem dim_fin_fun {K : Type u} [field K] (n : ) :
(fin n → K) = n

theorem exists_mem_ne_zero_of_ne_bot {K : Type u} {V : Type v} [field K] [ V] {s : V} :
s (∃ (b : V), b s b 0)

theorem exists_mem_ne_zero_of_dim_pos {K : Type u} {V : Type v} [field K] [ V] {s : V} :
0 < (∃ (b : V), b s b 0)

theorem exists_is_basis_fintype {K : Type u} {V : Type v} [field K] [ V] :
(∃ (s : set V), nonempty (fintype s))

def rank {K : Type u} {V : Type v} {V' : Type v'} [field K] [ V] [add_comm_group V'] [ V'] :
(V →ₗ[K] V')cardinal

rank f is the rank of a linear_map f, defined as the dimension of f.range.

Equations
theorem rank_le_domain {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :

theorem rank_le_range {K : Type u} {V V₁ : Type v} [field K] [ V] [add_comm_group V₁] [ V₁] (f : V →ₗ[K] V₁) :
rank f V₁

theorem rank_add_le {K : Type u} {V : Type v} {V' : Type v'} [field K] [ V] [add_comm_group V'] [ V'] (f g : V →ₗ[K] V') :
rank (f + g) rank f + rank g

@[simp]
theorem rank_zero {K : Type u} {V : Type v} {V' : Type v'} [field K] [ V] [add_comm_group V'] [ V'] :
rank 0 = 0

theorem rank_finset_sum_le {K : Type u} {V : Type v} {V' : Type v'} [field K] [ V] [add_comm_group V'] [ V'] {η : Type u_1} (s : finset η) (f : η → (V →ₗ[K] V')) :
rank (∑ (d : η) in s, f d) ∑ (d : η) in s, rank (f d)

theorem rank_comp_le1 {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [field K] [ V] [add_comm_group V'] [ V'] [add_comm_group V''] [ V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
rank (f.comp g) rank f

theorem rank_comp_le2 {K : Type u} {V : Type v} {V' V'₁ : Type v'} [field K] [ V] [add_comm_group V'] [ V'] [add_comm_group V'₁] [ V'₁] (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
rank (f.comp g) rank g

theorem dim_zero_iff_forall_zero {K : Type u} {V : Type v} [field K] [ V] :
= 0 ∀ (x : V), x = 0

theorem dim_pos_iff_exists_ne_zero {K : Type u} {V : Type v} [field K] [ V] :
0 < ∃ (x : V), x 0

theorem dim_pos_iff_nontrivial {K : Type u} {V : Type v} [field K] [ V] :
0 <

theorem dim_pos {K : Type u} {V : Type v} [field K] [ V] [h : nontrivial V] :
0 <

theorem dim_le_one_iff {K : Type u} {V : Type v} [field K] [ V] :
1 ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r v₀ = v

A vector space has dimension at most 1 if and only if there is a single vector of which all vectors are multiples.

theorem dim_submodule_le_one_iff {K : Type u} {V : Type v} [field K] [ V] (s : V) :
1 ∃ (v₀ : V) (H : v₀ s), s {v₀}

A submodule has dimension at most 1 if and only if there is a single vector in the submodule such that the submodule is contained in its span.

theorem dim_submodule_le_one_iff' {K : Type u} {V : Type v} [field K] [ V] (s : V) :
1 ∃ (v₀ : V), s {v₀}

A submodule has dimension at most 1 if and only if there is a single vector, not necessarily in the submodule, such that the submodule is contained in its span.

theorem linear_equiv.dim_eq_lift {K : Type u} {V : Type v} {E : Type v'} [field K] [ V] [ E] :
(V ≃ₗ[K] E) V).lift = E).lift

Version of linear_equiv.dim_eq without universe constraints.