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 Module.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.
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 M
over a field R
, this is the same as the finite dimension
of M
over R
.
Equations
- Module.finrank R M = Cardinal.toNat (Module.rank R M)
Instances For
Alias of Module.finrank
.
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 M
over a field R
, this is the same as the finite dimension
of M
over R
.
Equations
Instances For
This is like rank_eq_one_iff_finrank_eq_one
but works for 2
, 3
, 4
, ...
The dimension of a finite dimensional space is preserved under linear equivalence.
Pushforwards of finite-dimensional submodules along a LinearEquiv
have the same finrank.
The dimensions of the domain and range of an injective linear map are equal.