The finite-dimensional space of matrices #
This file shows that
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 field
matrix m n Ris
card m * card n
matrix, finite dimensional, findim, finrank
The dimension of the space of finite dimensional matrices is the product of the number of rows and columns.