# mathlibdocumentation

linear_algebra.matrix.finite_dimensional

# 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 field K
• matrix.finrank_matrix: the finrank of matrix m n R is card m * card n

## Tags #

matrix, finite dimensional, findim, finrank

@[instance]
def matrix.finite_dimensional {m : Type u_1} {n : Type u_2} [fintype m] [fintype n] {R : Type v} [field 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] :
(matrix m n R) =

The dimension of the space of finite dimensional matrices is the product of the number of rows and columns.