Finite dimensional vector spaces #
This file contains some further development of finite dimensional vector spaces, their dimensions, and linear maps on such spaces.
Definitions and results that require fewer imports are in
Mathlib.LinearAlgebra.FiniteDimensional.Defs
.
The dimension of a strict submodule is strictly bounded by the dimension of the ambient space.
The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t
Given isomorphic subspaces p q
of vector spaces V
and V₁
respectively,
p.quotient
is isomorphic to q.quotient
.
Equations
- FiniteDimensional.LinearEquiv.quotEquivOfEquiv f₁ f₂ = LinearEquiv.ofFinrankEq (V ⧸ p) (V₂ ⧸ q) ⋯
Instances For
Given the subspaces p q
, if p.quotient ≃ₗ[K] q
, then q.quotient ≃ₗ[K] p
Equations
Instances For
rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.
Given a linear map f
between two vector spaces with the same dimension, if
ker f = ⊥
then linearEquivOfInjective
is the induced isomorphism
between the two vector spaces.
Equations
- f.linearEquivOfInjective hf hdim = LinearEquiv.ofBijective f ⋯
Instances For
A linear independent family of finrank K V
vectors forms a basis.
Equations
- basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = Basis.mk lin_ind ⋯
Instances For
A linear independent finset of finrank K V
vectors forms a basis.
Equations
- finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯
Instances For
A linear independent set of finrank K V
vectors forms a basis.
Equations
- setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯
Instances For
We now give characterisations of finrank K V = 1
and finrank K V ≤ 1
.
Any K
-algebra module that is 1-dimensional over K
is simple.