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) (M : Type u_2) [Semiring R] [AddCommGroup M] [Module R M] :

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.

Instances For

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

    theorem LinearEquiv.finrank_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [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] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M ≃ₗ[R] M₂) (p : Submodule R M) :

    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.

    theorem Submodule.finrank_map_subtype_eq {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (q : Submodule R p) :