The finite-dimensional space of matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 finite_dimensional.
Main definitions #
matrix.finite_dimensional: matrices form a finite dimensional vector space over a fieldKlinear_map.finite_dimensional
Tags #
matrix, finite dimensional, findim, finrank
@[protected, instance]
def
matrix.finite_dimensional
{m : Type u_1}
{n : Type u_2}
{R : Type v}
[field R]
[finite m]
[finite n] :
finite_dimensional R (matrix m n R)
@[protected, instance]
def
linear_map.finite_dimensional
{K : Type u_1}
[field K]
{V : Type u_2}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_3}
[add_comm_group W]
[module K W]
[finite_dimensional K W] :
finite_dimensional K (V →ₗ[K] W)
@[protected, instance]
def
linear_map.finite_dimensional'
{K : Type u_1}
[field K]
{V : Type u_2}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_3}
[add_comm_group W]
[module K W]
[finite_dimensional K W]
{A : Type u_4}
[ring A]
[algebra K A]
[module A V]
[is_scalar_tower K A V]
[module A W]
[is_scalar_tower K A W] :
finite_dimensional 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.