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 field K
• LinearMap.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)

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)

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.