The finite-dimensional space of matrices #
This file shows that m by n matrices form a finite-dimensional space,
and proves the finrank of that space is equal to card m * card n.
Main definitions #
matrix.finite_dimensional: matrices form a finite dimensional vector space over a fieldKmatrix.finrank_matrix: thefinrankofmatrix m n Riscard m * card n
Tags #
matrix, finite dimensional, findim, finrank
@[protected, instance]
def
matrix.finite_dimensional
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
{R : Type v}
[field R] :
finite_dimensional R (matrix m n R)
@[simp]
theorem
matrix.finrank_matrix
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
{R : Type v}
[field R] :
finite_dimensional.finrank R (matrix m n R) = (fintype.card m) * fintype.card n
The dimension of the space of finite dimensional matrices is the product of the number of rows and columns.