mathlib3 documentation


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 #

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] :
@[protected, instance]
@[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] :

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.