The finite-dimensional space of matrices #
This file shows that m by n matrices form a finite-dimensional space.
Note that this is proven more generally elsewhere over modules as Module.Finite.matrix; this file
exists only to provide an entry in the instance list for FiniteDimensional.
Main definitions #
Matrix.finiteDimensional: matrices form a finite dimensional vector space over a fieldKLinearMap.finiteDimensional
Tags #
matrix, finite dimensional, findim, finrank
instance
Matrix.finiteDimensional
{m : Type u_1}
{n : Type u_2}
{R : Type v}
[Field R]
[Finite m]
[Finite n]
:
FiniteDimensional R (Matrix m n R)
Equations
- (_ : FiniteDimensional R (Matrix m n R)) = (_ : Module.Finite R (Matrix m n R))
instance
LinearMap.finiteDimensional
{K : Type u_1}
[Field K]
{V : Type u_2}
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
{W : Type u_3}
[AddCommGroup W]
[Module K W]
[FiniteDimensional K W]
:
FiniteDimensional K (V →ₗ[K] W)
Equations
- (_ : FiniteDimensional K (V →ₗ[K] W)) = (_ : Module.Finite K (V →ₗ[K] W))
instance
LinearMap.finiteDimensional'
{K : Type u_1}
[Field K]
{V : Type u_2}
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
{W : Type u_3}
[AddCommGroup W]
[Module K W]
[FiniteDimensional K W]
{A : Type u_4}
[Ring A]
[Algebra K A]
[Module A V]
[IsScalarTower K A V]
[Module A W]
[IsScalarTower K A W]
:
FiniteDimensional K (V →ₗ[A] W)
Linear maps over a k-algebra are finite dimensional (over k) if both the source and
target are, as they form a subspace of all k-linear maps.
Equations
- (_ : FiniteDimensional K (V →ₗ[A] W)) = (_ : FiniteDimensional K (V →ₗ[A] W))