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 lift
s. The types V
, V'
, ... all live in different universes,
and V₁
, V₂
, ... all live in the same universe.
the dimension of a vector space, defined as a term of type cardinal
Equations
- vector_space.dim K V = cardinal.min _ (λ (b : {b // is_basis K (λ (i : ↥b), ↑i)}), # ↥(b.val))
dimension theorem
Two linearly equivalent vector spaces have the same dimension, a version with different universes.
Two linearly equivalent vector spaces have the same dimension.
Two vector spaces are isomorphic if they have the same dimension.
Two vector spaces are isomorphic if they have the same dimension.
Two vector spaces are isomorphic if they have the same dimension.
Equations
- linear_equiv.of_lift_dim_eq V V' cond = classical.choice _
Two vector spaces are isomorphic if they have the same dimension.
Equations
- linear_equiv.of_dim_eq V V₁ cond = classical.choice _
Two vector spaces are isomorphic if and only if they have the same dimension.
Two vector spaces are isomorphic if and only if they have the same dimension.
rank-nullity theorem
This is mostly an auxiliary lemma for dim_sup_add_dim_inf_eq
.
rank f
is the rank of a linear_map f
, defined as the dimension of f.range
.
Equations
- rank f = vector_space.dim K ↥(f.range)
A vector space has dimension at most 1
if and only if there is a
single vector of which all vectors are multiples.
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.
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.
Version of linear_equiv.dim_eq without universe constraints.