# Documentation

Mathlib.LinearAlgebra.Finrank

# Finite dimension of vector spaces #

Definition of the rank of a module, or dimension of a vector space, as a natural number.

## Main definitions #

Defined is FiniteDimensional.finrank, the dimension of a finite dimensional space, returning a Nat, as opposed to Module.rank, which returns a Cardinal. When the space has infinite dimension, its finrank is by convention set to 0.

The definition of finrank does not assume a FiniteDimensional instance, but lemmas might. Import LinearAlgebra.FiniteDimensional to get access to these additional lemmas.

Formulas for the dimension are given for linear equivs, in LinearEquiv.finrank_eq.

## Implementation notes #

Most results are deduced from the corresponding results for the general dimension (as a cardinal), in Dimension.lean. Not all results have been ported yet.

You should not assume that there has been any effort to state lemmas as generally as possible.

noncomputable def FiniteDimensional.finrank (R : Type u_1) (V : Type u_2) [] [] [Module R V] :

The rank of a module as a natural number.

Defined by convention to be 0 if the space has infinite rank.

For a vector space V over a field K, this is the same as the finite dimension of V over K.

Instances For
theorem FiniteDimensional.finrank_eq_of_rank_eq {K : Type u} {V : Type v} [Ring K] [] [Module K V] {n : } (h : = n) :
theorem FiniteDimensional.rank_eq_ofNat_iff_finrank_eq_ofNat {K : Type u} {V : Type v} [Ring K] [] [Module K V] (n : ) [] :
=

This is like rank_eq_one_iff_finrank_eq_one but works for 2, 3, 4, ...

theorem FiniteDimensional.finrank_le_of_rank_le {K : Type u} {V : Type v} [Ring K] [] [Module K V] {n : } (h : n) :
theorem FiniteDimensional.finrank_lt_of_rank_lt {K : Type u} {V : Type v} [Ring K] [] [Module K V] {n : } (h : < n) :
theorem FiniteDimensional.lt_rank_of_lt_finrank {K : Type u} {V : Type v} [Ring K] [] [Module K V] {n : } (h : ) :
n <
theorem FiniteDimensional.one_lt_rank_of_one_lt_finrank {K : Type u} {V : Type v} [Ring K] [] [Module K V] (h : ) :
1 <
theorem FiniteDimensional.finrank_le_finrank_of_rank_le_rank {K : Type u} {V : Type v} [Ring K] [] [Module K V] {V₂ : Type v'} [] [Module K V₂] (h : ) (h' : ) :
theorem FiniteDimensional.nontrivial_of_finrank_pos {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] [] (h : ) :

A finite dimensional space is nontrivial if it has positive finrank.

theorem FiniteDimensional.nontrivial_of_finrank_eq_succ {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] [] {n : } (hn : ) :

A finite dimensional space is nontrivial if it has finrank equal to the successor of a natural number.

theorem FiniteDimensional.finrank_zero_of_subsingleton {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] [] [h : ] :

A (finite dimensional) space that is a subsingleton has zero finrank.

theorem FiniteDimensional.finrank_eq_card_basis {K : Type u} {V : Type v} [Ring K] [] [Module K V] {ι : Type w} [] (h : Basis ι K V) :

If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis.

theorem FiniteDimensional.finrank_eq_card_finset_basis {K : Type u} {V : Type v} [Ring K] [] [Module K V] {ι : Type w} {b : } (h : Basis { x // x b } K V) :

If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis. This lemma uses a Finset instead of indexed types.

@[simp]

A ring satisfying StrongRankCondition (such as a DivisionRing) is one-dimensional as a module over itself.

@[simp]

The vector space of functions on a Fintype ι has finrank equal to the cardinality of ι.

The vector space of functions on Fin n has finrank equal to n.

theorem FiniteDimensional.Basis.subset_extend {K : Type u} {V : Type v} [] [] [Module K V] {s : Set V} (hs : LinearIndependent K Subtype.val) :
s LinearIndependent.extend hs (_ : s Set.univ)
theorem finrank_eq_zero_of_basis_imp_not_finite {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (h : ∀ (s : Set V), Basis (s) K V) :
theorem finrank_eq_zero_of_basis_imp_false {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (h : ∀ (s : ), Basis (s) K VFalse) :
theorem finrank_eq_zero_of_not_exists_basis {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (h : ¬s, Nonempty (Basis (s) K V)) :
theorem finrank_eq_zero_of_not_exists_basis_finite {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (h : ¬s x, ) :
theorem finrank_eq_zero_of_not_exists_basis_finset {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (h : ¬s, Nonempty (Basis { x // x s } K V)) :
theorem LinearEquiv.finrank_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [] [] [Module R M] [Module R M₂] (f : M ≃ₗ[R] M₂) :

The dimension of a finite dimensional space is preserved under linear equivalence.

theorem LinearEquiv.finrank_map_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [] [] [Module R M] [Module R M₂] (f : M ≃ₗ[R] M₂) (p : ) :

Pushforwards of finite-dimensional submodules along a LinearEquiv have the same finrank.

theorem LinearMap.finrank_range_of_inj {K : Type u} {V : Type v} [Ring K] [] [Module K V] {V₂ : Type v'} [] [Module K V₂] {f : V →ₗ[K] V₂} (hf : ) :

The dimensions of the domain and range of an injective linear map are equal.

@[simp]
theorem finrank_bot (K : Type u) (V : Type v) [Ring K] [] [Module K V] [] :
@[simp]
theorem finrank_top (K : Type u) (V : Type v) [Ring K] [] [Module K V] :
theorem Submodule.lt_of_le_of_finrank_lt_finrank {K : Type u} {V : Type v} [Ring K] [] [Module K V] {s : } {t : } (le : s t) (lt : FiniteDimensional.finrank K { x // x s } < FiniteDimensional.finrank K { x // x t }) :
s < t
theorem Submodule.lt_top_of_finrank_lt_finrank {K : Type u} {V : Type v} [Ring K] [] [Module K V] {s : } (lt : FiniteDimensional.finrank K { x // x s } < ) :
s <
noncomputable def Set.finrank (K : Type u) {V : Type v} [] [] [Module K V] (s : Set V) :

The rank of a set of vectors as a natural number.

Instances For
theorem finrank_span_le_card {K : Type u} {V : Type v} [] [] [Module K V] (s : Set V) [Fintype s] :
theorem finrank_span_finset_le_card {K : Type u} {V : Type v} [] [] [Module K V] (s : ) :
theorem finrank_range_le_card {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] {b : ιV} :
theorem finrank_span_eq_card {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] {b : ιV} (hb : ) :
theorem finrank_span_set_eq_card {K : Type u} {V : Type v} [] [] [Module K V] (s : Set V) [Fintype s] (hs : LinearIndependent K Subtype.val) :
theorem finrank_span_finset_eq_card {K : Type u} {V : Type v} [] [] [Module K V] (s : ) (hs : LinearIndependent K Subtype.val) :
theorem span_lt_of_subset_of_card_lt_finrank {K : Type u} {V : Type v} [] [] [Module K V] {s : Set V} [Fintype s] {t : } (subset : s t) (card_lt : < FiniteDimensional.finrank K { x // x t }) :
< t
theorem span_lt_top_of_card_lt_finrank {K : Type u} {V : Type v} [] [] [Module K V] {s : Set V} [Fintype s] (card_lt : ) :
theorem exists_linearIndependent_snoc_of_lt_finrank {K : Type u} {V : Type v} [] [] [Module K V] {n : } {v : Fin nV} (hv : ) (h : ) :

Given a family of n linearly independent vectors in a finite-dimensional space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_cons_of_lt_finrank {K : Type u} {V : Type v} [] [] [Module K V] {n : } {v : Fin nV} (hv : ) (h : ) :

Given a family of n linearly independent vectors in a finite-dimensional space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_pair_of_one_lt_finrank {K : Type u} {V : Type v} [] [] [Module K V] (h : ) {x : V} (hx : x 0) :
y, LinearIndependent K ![x, y]

Given a nonzero vector in a finite-dimensional space of dimension > 1, one may find another vector linearly independent of the first one.

theorem linearIndependent_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] {b : ιV} (spans : ) (card_eq : ) :
theorem linearIndependent_iff_card_eq_finrank_span {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] {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_1} [] {b : ιV} :
noncomputable def basisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] (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.

Instances For
@[simp]
theorem coe_basisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {ι : Type u_1} [] (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 : ) :
∀ (a : V), (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ↑(LinearIndependent.repr (_ : LinearIndependent K Subtype.val)) (↑(LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id (_ : ∀ (x : V), LinearMap.id x Submodule.span K (Set.range Subtype.val))) a)
noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {s : } (le_span : ) (card_eq : ) :
Basis (s) K V

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

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 : ) :
∀ (a : V), (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = ↑(LinearIndependent.repr (_ : LinearIndependent K Subtype.val)) (↑(LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id (_ : ∀ (x : V), LinearMap.id x Submodule.span K (Set.range Subtype.val))) a)
noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [] [] [Module K V] {s : Set V} [Fintype s] (le_span : ) (card_eq : ) :
Basis (s) K V

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

Instances For

We now give characterisations of finrank K V = 1 and finrank K V ≤ 1.

theorem finrank_eq_one {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (v : V) (n : v 0) (h : ∀ (w : V), c, c v = w) :

If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

theorem finrank_le_one {K : Type u} {V : Type v} [Ring K] [] [Module K V] [] (v : V) (h : ∀ (w : V), c, c v = w) :

If every vector is a multiple of some v : V, then V has dimension at most one.

@[simp]
theorem Subalgebra.rank_toSubmodule {F : Type u_1} {E : Type u_2} [] [Ring E] [Algebra F E] (S : ) :
Module.rank F { x // x Subalgebra.toSubmodule S } = Module.rank F { x // x S }
@[simp]
theorem Subalgebra.finrank_toSubmodule {F : Type u_1} {E : Type u_2} [] [Ring E] [Algebra F E] (S : ) :
FiniteDimensional.finrank F { x // x Subalgebra.toSubmodule S } = FiniteDimensional.finrank F { x // x S }
theorem subalgebra_top_rank_eq_submodule_top_rank {F : Type u_1} {E : Type u_2} [] [Ring E] [Algebra F E] :
Module.rank F { x // x } = Module.rank F { x // x }
theorem Subalgebra.rank_top {F : Type u_1} {E : Type u_2} [] [Ring E] [Algebra F E] :
Module.rank F { x // x } =
@[simp]
theorem Subalgebra.rank_bot {F : Type u_1} {E : Type u_2} [] [Ring E] [Algebra F E] [] [] :
Module.rank F { x // x } = 1
@[simp]
theorem Subalgebra.finrank_bot {F : Type u_1} {E : Type u_2} [] [Ring E] [Algebra F E] [] [] :