Linear maps and matrices
This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.
Some results are proved about the linear map corresponding to a
diagonal matrix (range, ker and rank).
Main definitions
to_lin, to_matrix, linear_equiv_matrix
Tags
linear_map, matrix, linear_equiv, diagonal
@[instance]
def
matrix.fintype
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
(R : Type u_1)
[fintype R] :
Equations
- matrix.fintype R = _.mpr pi.fintype
Evaluation of matrices gives a linear map from matrix m n R to
linear maps (n → R) →ₗ[R] (m → R).
Equations
- matrix.eval = linear_map.mk₂ R matrix.mul_vec matrix.eval._proof_1 matrix.eval._proof_2 matrix.eval._proof_3 matrix.eval._proof_4
def
matrix.to_lin
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R] :
Evaluation of matrices gives a map from matrix m n R to
linear maps (n → R) →ₗ[R] (m → R).
Equations
theorem
matrix.to_lin_of_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
{p : Type u_1}
{q : Type u_4}
[fintype p]
[fintype q]
(e₁ : m ≃ p)
(e₂ : n ≃ q)
(f : matrix p q R) :
matrix.to_lin (λ (i : m) (j : n), f (⇑e₁ i) (⇑e₂ j)) = ⇑((linear_map.fun_congr_left R R e₂).arrow_congr (linear_map.fun_congr_left R R e₁)) f.to_lin
@[instance]
def
matrix.to_lin.is_add_monoid_hom
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R] :
Equations
@[simp]
def
linear_map.to_matrixₗ
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n] :
The linear map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R.
def
linear_map.to_matrix
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n] :
The map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R.
Equations
@[simp]
theorem
linear_map.to_matrix_id
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n] :
theorem
linear_map.to_matrix_of_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
{p : Type u_1}
{q : Type u_4}
[decidable_eq n]
[decidable_eq q]
[fintype p]
[fintype q]
(e₁ : m ≃ p)
(e₂ : n ≃ q)
(f : (q → R) →ₗ[R] p → R)
(i : m)
(j : n) :
f.to_matrix (⇑e₁ i) (⇑e₂ j) = (⇑((linear_map.fun_congr_left R R e₂).arrow_congr (linear_map.fun_congr_left R R e₁)) f).to_matrix i j
theorem
to_lin_to_matrix
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
{M : matrix m n R} :
to_lin is the right inverse of to_matrix.
def
linear_equiv_matrix'
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n] :
Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R.
Equations
- linear_equiv_matrix' = {to_fun := linear_map.to_matrix (λ (a b : n), _inst_5 a b), map_add' := _, map_smul' := _, inv_fun := matrix.to_lin _inst_4, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv_matrix'_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(f : (n → R) →ₗ[R] m → R) :
def
linear_equiv_matrix
{R : Type v}
[comm_ring R]
{ι : Type u_4}
{κ : Type u_5}
{M₁ : Type u_6}
{M₂ : Type u_7}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[fintype ι]
[decidable_eq ι]
[fintype κ]
{v₁ : ι → M₁}
{v₂ : κ → M₂} :
Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear
equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.
Equations
- linear_equiv_matrix hv₁ hv₂ = ((equiv_fun_basis hv₁).arrow_congr (equiv_fun_basis hv₂)).trans linear_equiv_matrix'
theorem
linear_equiv_matrix_apply
{R : Type v}
[comm_ring R]
{ι : Type u_4}
{κ : Type u_5}
{M₁ : Type u_6}
{M₂ : Type u_7}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[fintype ι]
[decidable_eq ι]
[fintype κ]
{v₁ : ι → M₁}
{v₂ : κ → M₂}
(hv₁ : is_basis R v₁)
(hv₂ : is_basis R v₂)
(f : M₁ →ₗ[R] M₂)
(i : κ)
(j : ι) :
⇑(linear_equiv_matrix hv₁ hv₂) f i j = ⇑(equiv_fun_basis hv₂) (⇑f (v₁ j)) i
theorem
linear_equiv_matrix_apply'
{R : Type v}
[comm_ring R]
{ι : Type u_4}
{κ : Type u_5}
{M₁ : Type u_6}
{M₂ : Type u_7}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[fintype ι]
[decidable_eq ι]
[fintype κ]
{v₁ : ι → M₁}
{v₂ : κ → M₂}
(hv₁ : is_basis R v₁)
(hv₂ : is_basis R v₂)
(f : M₁ →ₗ[R] M₂)
(i : κ)
(j : ι) :
@[simp]
theorem
linear_equiv_matrix_id
{R : Type v}
[comm_ring R]
{ι : Type u_4}
{M₁ : Type u_6}
[add_comm_group M₁]
[module R M₁]
[fintype ι]
[decidable_eq ι]
{v₁ : ι → M₁}
(hv₁ : is_basis R v₁) :
⇑(linear_equiv_matrix hv₁ hv₁) linear_map.id = 1
@[simp]
theorem
linear_equiv_matrix_symm_one
{R : Type v}
[comm_ring R]
{ι : Type u_4}
{M₁ : Type u_6}
[add_comm_group M₁]
[module R M₁]
[fintype ι]
[decidable_eq ι]
{v₁ : ι → M₁}
(hv₁ : is_basis R v₁) :
⇑((linear_equiv_matrix hv₁ hv₁).symm) 1 = linear_map.id
theorem
linear_equiv_matrix_range
{R : Type v}
[comm_ring R]
{ι : Type u_4}
{κ : Type u_5}
{M₁ : Type u_6}
{M₂ : Type u_7}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[fintype ι]
[decidable_eq ι]
[fintype κ]
{v₁ : ι → M₁}
{v₂ : κ → M₂}
(hv₁ : is_basis R v₁)
(hv₂ : is_basis R v₂)
(f : M₁ →ₗ[R] M₂)
(k : κ)
(i : ι) :
⇑(linear_equiv_matrix _ _) f ⟨v₂ k, _⟩ ⟨v₁ i, _⟩ = ⇑(linear_equiv_matrix hv₁ hv₂) f k i
theorem
matrix.linear_equiv_matrix_comp
{R : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
{μ : Type u_7}
{M₁ : Type u_8}
{M₂ : Type u_9}
{M₃ : Type u_10}
[comm_ring R]
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[add_comm_group M₃]
[module R M₃]
[fintype ι]
[decidable_eq κ]
[fintype κ]
[fintype μ]
{v₁ : ι → M₁}
{v₂ : κ → M₂}
{v₃ : μ → M₃}
(hv₁ : is_basis R v₁)
(hv₂ : is_basis R v₂)
(hv₃ : is_basis R v₃)
[decidable_eq ι]
(f : M₂ →ₗ[R] M₃)
(g : M₁ →ₗ[R] M₂) :
⇑(linear_equiv_matrix hv₁ hv₃) (f.comp g) = (⇑(linear_equiv_matrix hv₂ hv₃) f).mul (⇑(linear_equiv_matrix hv₁ hv₂) g)
theorem
matrix.linear_equiv_matrix_mul
{R : Type u_4}
{ι : Type u_5}
{M₁ : Type u_8}
[comm_ring R]
[add_comm_group M₁]
[module R M₁]
[fintype ι]
{v₁ : ι → M₁}
(hv₁ : is_basis R v₁)
[decidable_eq ι]
(f g : M₁ →ₗ[R] M₁) :
⇑(linear_equiv_matrix hv₁ hv₁) (f * g) = ⇑(linear_equiv_matrix hv₁ hv₁) f * ⇑(linear_equiv_matrix hv₁ hv₁) g
theorem
matrix.linear_equiv_matrix_symm_mul
{R : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
{μ : Type u_7}
{M₁ : Type u_8}
{M₂ : Type u_9}
{M₃ : Type u_10}
[comm_ring R]
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
[add_comm_group M₃]
[module R M₃]
[fintype ι]
[decidable_eq κ]
[fintype κ]
[fintype μ]
{v₁ : ι → M₁}
{v₂ : κ → M₂}
{v₃ : μ → M₃}
(hv₁ : is_basis R v₁)
(hv₂ : is_basis R v₂)
(hv₃ : is_basis R v₃)
[decidable_eq μ]
(A : matrix ι κ R)
(B : matrix κ μ R) :
⇑((linear_equiv_matrix hv₃ hv₁).symm) (A.mul B) = (⇑((linear_equiv_matrix hv₂ hv₁).symm) A).comp (⇑((linear_equiv_matrix hv₃ hv₂).symm) B)
theorem
matrix.linear_equiv.is_unit_det
{R : Type u_4}
{ι : Type u_5}
{M : Type u_6}
{M' : Type u_7}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group M']
[module R M']
[decidable_eq ι]
[fintype ι]
{v : ι → M}
{v' : ι → M'}
(f : M ≃ₗ[R] M')
(hv : is_basis R v)
(hv' : is_basis R v') :
is_unit (⇑(linear_equiv_matrix hv hv') ↑f).det
def
matrix.linear_equiv.of_is_unit_det
{R : Type u_4}
{ι : Type u_5}
{M : Type u_6}
{M' : Type u_7}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group M']
[module R M']
[decidable_eq ι]
[fintype ι]
{v : ι → M}
{v' : ι → M'}
{f : M →ₗ[R] M'}
{hv : is_basis R v}
{hv' : is_basis R v'} :
Builds a linear equivalence from a linear map whose determinant in some bases is a unit.
def
matrix.diag
(n : Type u_3)
[fintype n]
(R : Type v)
(M : Type w)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
The diagonal of a square matrix.
@[simp]
theorem
matrix.diag_apply
{n : Type u_3}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(A : matrix n n M)
(i : n) :
⇑(matrix.diag n R M) A i = A i i
@[simp]
theorem
matrix.diag_one
{n : Type u_3}
[fintype n]
{R : Type v}
[semiring R]
[decidable_eq n] :
⇑(matrix.diag n R R) 1 = λ (i : n), 1
@[simp]
theorem
matrix.diag_transpose
{n : Type u_3}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(A : matrix n n M) :
⇑(matrix.diag n R M) A.transpose = ⇑(matrix.diag n R M) A
def
matrix.trace
(n : Type u_3)
[fintype n]
(R : Type v)
(M : Type w)
[semiring R]
[add_comm_monoid M]
[semimodule R M] :
The trace of a square matrix.
Equations
- matrix.trace n R M = {to_fun := λ (A : matrix n n M), finset.univ.sum (λ (i : n), ⇑(matrix.diag n R M) A i), map_add' := _, map_smul' := _}
@[simp]
theorem
matrix.trace_diag
{n : Type u_3}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(A : matrix n n M) :
⇑(matrix.trace n R M) A = finset.univ.sum (λ (i : n), ⇑(matrix.diag n R M) A i)
@[simp]
theorem
matrix.trace_one
{n : Type u_3}
[fintype n]
{R : Type v}
[semiring R]
[decidable_eq n] :
⇑(matrix.trace n R R) 1 = ↑(fintype.card n)
@[simp]
theorem
matrix.trace_transpose
{n : Type u_3}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[semimodule R M]
(A : matrix n n M) :
⇑(matrix.trace n R M) A.transpose = ⇑(matrix.trace n R M) A
theorem
matrix.trace_mul_comm
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{S : Type v}
[comm_ring S]
(A : matrix m n S)
(B : matrix n m S) :
⇑(matrix.trace n S S) (B.mul A) = ⇑(matrix.trace m S S) (A.mul B)
theorem
matrix.proj_diagonal
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(i : n)
(w : n → R) :
(linear_map.proj i).comp (matrix.diagonal w).to_lin = w i • linear_map.proj i
theorem
matrix.diagonal_comp_std_basis
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(w : n → R)
(i : n) :
(matrix.diagonal w).to_lin.comp (linear_map.std_basis R (λ (_x : n), R) i) = w i • linear_map.std_basis R (λ (_x : n), R) i
theorem
matrix.diagonal_to_lin
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(w : n → R) :
(matrix.diagonal w).to_lin = linear_map.pi (λ (i : n), w i • linear_map.proj i)
def
matrix.to_linear_equiv
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(P : matrix n n R) :
An invertible matrix yields a linear equivalence from the free module to itself.
@[simp]
theorem
matrix.to_linear_equiv_apply
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(P : matrix n n R)
(h : is_unit P) :
↑(P.to_linear_equiv h) = P.to_lin
@[simp]
theorem
matrix.to_linear_equiv_symm_apply
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n]
(P : matrix n n R)
(h : is_unit P) :
theorem
matrix.rank_vec_mul_vec
{K : Type u}
[field K]
{m n : Type u}
[fintype m]
[fintype n]
(w : m → K)
(v : n → K) :
rank (matrix.vec_mul_vec w v).to_lin ≤ 1
theorem
matrix.ker_diagonal_to_lin
{m : Type u_2}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
(w : m → K) :
(matrix.diagonal w).to_lin.ker = ⨆ (i : m) (H : i ∈ {i : m | w i = 0}), (linear_map.std_basis K (λ (i : m), K) i).range
theorem
matrix.range_diagonal
{m : Type u_2}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
(w : m → K) :
(matrix.diagonal w).to_lin.range = ⨆ (i : m) (H : i ∈ {i : m | w i ≠ 0}), (linear_map.std_basis K (λ (i : m), K) i).range
theorem
matrix.rank_diagonal
{m : Type u_2}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
[decidable_eq K]
(w : m → K) :
rank (matrix.diagonal w).to_lin = ↑(fintype.card {i // w i ≠ 0})
@[instance]
def
matrix.finite_dimensional
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[field R] :
finite_dimensional R (matrix m n R)
Equations
@[simp]
theorem
matrix.findim_matrix
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[field R] :
finite_dimensional.findim 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.
def
matrix.reindex
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{m' : Type u_5}
{n' : Type u_6}
[fintype m']
[fintype n']
{R : Type v} :
The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.
def
matrix.reindex_linear_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{m' : Type u_5}
{n' : Type u_6}
[fintype m']
[fintype n']
{R : Type v}
[semiring R] :
The natural map that reindexes a matrix's rows and columns with equivalent types is a linear equivalence.
Equations
- matrix.reindex_linear_equiv eₘ eₙ = {to_fun := (matrix.reindex eₘ eₙ).to_fun, map_add' := _, map_smul' := _, inv_fun := (matrix.reindex eₘ eₙ).inv_fun, left_inv := _, right_inv := _}
theorem
matrix.reindex_mul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
[fintype l]
[fintype m]
[fintype n]
{l' : Type u_4}
{m' : Type u_5}
{n' : Type u_6}
[fintype l']
[fintype m']
[fintype n']
{R : Type v}
[semiring R]
(eₘ : m ≃ m')
(eₙ : n ≃ n')
(eₗ : l ≃ l')
(M : matrix m n R)
(N : matrix n l R) :
(⇑(matrix.reindex_linear_equiv eₘ eₙ) M).mul (⇑(matrix.reindex_linear_equiv eₙ eₗ) N) = ⇑(matrix.reindex_linear_equiv eₘ eₗ) (M.mul N)
def
matrix.reindex_alg_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_semiring R]
[decidable_eq m]
[decidable_eq n] :
For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence of algebras.
Equations
- matrix.reindex_alg_equiv e = {to_fun := (matrix.reindex_linear_equiv e e).to_fun, inv_fun := (matrix.reindex_linear_equiv e e).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
matrix.reindex_alg_equiv_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_semiring R]
[decidable_eq m]
[decidable_eq n]
(e : m ≃ n)
(M : matrix m m R) :
@[simp]
theorem
matrix.reindex_alg_equiv_symm_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_semiring R]
[decidable_eq m]
[decidable_eq n]
(e : m ≃ n)
(M : matrix n n R) :
def
linear_map.trace_aux
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
{b : ι → M} :
The trace of an endomorphism given a basis.
Equations
- linear_map.trace_aux R hb = (matrix.trace ι R R).comp ↑(linear_equiv_matrix hb hb)
@[simp]
theorem
linear_map.trace_aux_def
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
{b : ι → M}
(hb : is_basis R b)
(f : M →ₗ[R] M) :
⇑(linear_map.trace_aux R hb) f = ⇑(matrix.trace ι R R) (⇑(linear_equiv_matrix hb hb) f)
theorem
linear_map.trace_aux_eq'
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
{b : ι → M}
(hb : is_basis R b)
{κ : Type w}
[decidable_eq κ]
[fintype κ]
{c : κ → M}
(hc : is_basis R c) :
linear_map.trace_aux R hb = linear_map.trace_aux R hc
theorem
linear_map.trace_aux_range
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[fintype ι]
{b : ι → M}
(hb : is_basis R b) :
linear_map.trace_aux R _ = linear_map.trace_aux R hb
theorem
linear_map.trace_aux_eq
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type u_1}
[decidable_eq ι]
[fintype ι]
{b : ι → M}
(hb : is_basis R b)
{κ : Type u_2}
[decidable_eq κ]
[fintype κ]
{c : κ → M}
(hc : is_basis R c) :
linear_map.trace_aux R hb = linear_map.trace_aux R hc
where ι and κ can reside in different universes
Trace of an endomorphism independent of basis.
theorem
linear_map.trace_eq_matrix_trace
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[fintype ι]
{b : ι → M}
(hb : is_basis R b)
(f : M →ₗ[R] M) :
⇑(linear_map.trace R M) f = ⇑(matrix.trace ι R R) (⇑(linear_equiv_matrix hb hb) f)
theorem
linear_map.trace_mul_comm
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
(f g : M →ₗ[R] M) :
⇑(linear_map.trace R M) (f * g) = ⇑(linear_map.trace R M) (g * f)
def
alg_equiv_matrix'
{n : Type u_3}
[fintype n]
{R : Type v}
[comm_ring R]
[decidable_eq n] :
module.End R (n → R) ≃ₐ[R] matrix n n R
The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the algebra structures.
Equations
- alg_equiv_matrix' = {to_fun := linear_equiv_matrix'.to_fun, inv_fun := linear_equiv_matrix'.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
def
linear_equiv.alg_conj
{R : Type v}
[comm_ring R]
{M₁ : Type u_1}
{M₂ : Type (max u_2 u_3)}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂] :
(M₁ ≃ₗ[R] M₂) → (module.End R M₁ ≃ₐ[R] module.End R M₂)
A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.
def
alg_equiv_matrix
{n : Type u_3}
[fintype n]
{R : Type v}
{M : Type w}
[comm_ring R]
[add_comm_group M]
[module R M]
[decidable_eq n]
{b : n → M} :
is_basis R b → (module.End R M ≃ₐ[R] matrix n n R)
A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.