Dimension of vector spaces #
In this file we provide results about Module.rank
and Module.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
: ifV₁
is a submodule ofV
, thenModule.rank (V/V₁) + Module.rank V₁ = Module.rank V
.rank_range_add_rank_ker
: the rank-nullity theorem.
See also Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
for the Erdős-Kaplansky theorem.
If a vector space has a finite dimension, the index set of Basis.ofVectorSpace
is finite.
Also see rank_quotient_add_rank
.
This is mostly an auxiliary lemma for Submodule.rank_sup_add_rank_inf_eq
.
A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.
A family of finrank K V
vectors forms a basis if they span the whole space.
Equations
- basisOfTopLeSpanOfCardEqFinrank b le_span card_eq = Basis.mk ⋯ le_span
Instances For
A finset of finrank K V
vectors forms a basis if they span the whole space.
Equations
- finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq = basisOfTopLeSpanOfCardEqFinrank Subtype.val ⋯ ⋯
Instances For
A set of finrank K V
vectors forms a basis if they span the whole space.
Equations
- setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq = basisOfTopLeSpanOfCardEqFinrank Subtype.val ⋯ ⋯