mathlib documentation

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 #

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] :
@[simp]
theorem matrix.finrank_matrix {m : Type u_1} {n : Type u_2} [fintype m] [fintype n] {R : Type v} [field R] :

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