mathlib documentation

linear_algebra.matrix

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.

It also defines the trace of an endomorphism, and the determinant of a family of vectors with respect to some basis.

Some results are proved about the linear map corresponding to a diagonal matrix (range, ker and rank).

Main definitions

In the list below, and in all this file, R is a commutative ring (semiring is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite types used for indexing.

Tags

linear_map, matrix, linear_equiv, diagonal, det, trace

@[instance]
def matrix.fintype {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (R : Type u_1) [fintype R] :
fintype (matrix m n R)

Equations
def matrix.mul_vec_lin {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] :
matrix m n R((n → R) →ₗ[R] m → R)

matrix.mul_vec M is a linear map.

Equations
@[simp]
theorem matrix.mul_vec_lin_apply {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] (M : matrix m n R) (v : n → R) :

@[simp]
theorem matrix.mul_vec_std_basis {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] (M : matrix m n R) (i : m) (j : n) :
M.mul_vec ((linear_map.std_basis R (λ (_x : n), R) j) 1) i = M i j

def linear_map.to_matrix' {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] :
((n → R) →ₗ[R] m → R) ≃ₗ[R] matrix m n R

Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R.

Equations
def matrix.to_lin' {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] :
matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R

A matrix m n R is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R).

Equations
@[simp]
theorem linear_map.to_matrix'_symm {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] :

@[simp]
theorem matrix.to_lin'_symm {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] :

@[simp]
theorem linear_map.to_matrix'_to_lin' {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] (M : matrix m n R) :

@[simp]
theorem matrix.to_lin'_to_matrix' {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] (f : (n → R) →ₗ[R] m → R) :

@[simp]
theorem linear_map.to_matrix'_apply {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] (f : (n → R) →ₗ[R] m → R) (i : m) (j : n) :
linear_map.to_matrix' f i j = f (λ (j' : n), ite (j' = j) 1 0) i

@[simp]
theorem matrix.to_lin'_apply {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] (M : matrix m n R) (v : n → R) :

@[simp]
theorem matrix.to_lin'_one {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] :

@[simp]
theorem linear_map.to_matrix'_id {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] :

@[simp]
theorem matrix.to_lin'_mul {R : Type u_1} [comm_ring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] [decidable_eq n] [decidable_eq m] (M : matrix l m R) (N : matrix m n R) :

theorem linear_map.to_matrix'_comp {R : Type u_1} [comm_ring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] [decidable_eq n] [decidable_eq l] (f : (n → R) →ₗ[R] m → R) (g : (l → R) →ₗ[R] n → R) :

theorem linear_map.to_matrix'_mul {R : Type u_1} [comm_ring R] {m : Type u_3} [fintype m] [decidable_eq m] (f g : (m → R) →ₗ[R] m → R) :

def linear_map.to_matrix {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} :
is_basis R v₂((M₁ →ₗ[R] M₂) ≃ₗ[R] matrix m n R)

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
def matrix.to_lin {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} :
is_basis R v₂(matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂)

Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between matrices over R indexed by the bases and linear maps M₁ →ₗ M₂.

Equations
@[simp]
theorem linear_map.to_matrix_symm {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) :
(linear_map.to_matrix hv₁ hv₂).symm = matrix.to_lin hv₁ hv₂

@[simp]
theorem matrix.to_lin_symm {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) :
(matrix.to_lin hv₁ hv₂).symm = linear_map.to_matrix hv₁ hv₂

@[simp]
theorem matrix.to_lin_to_matrix {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) (f : M₁ →ₗ[R] M₂) :
(matrix.to_lin hv₁ hv₂) ((linear_map.to_matrix hv₁ hv₂) f) = f

@[simp]
theorem linear_map.to_matrix_to_lin {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) (M : matrix m n R) :
(linear_map.to_matrix hv₁ hv₂) ((matrix.to_lin hv₁ hv₂) M) = M

theorem linear_map.to_matrix_apply {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
(linear_map.to_matrix hv₁ hv₂) f i j = (hv₂.equiv_fun) (f (v₁ j)) i

theorem linear_map.to_matrix_apply' {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
(linear_map.to_matrix hv₁ hv₂) f i j = ((hv₂.repr) (f (v₁ j))) i

theorem matrix.to_lin_apply {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) (M : matrix m n R) (v : M₁) :
((matrix.to_lin hv₁ hv₂) M) v = ∑ (j : m), M.mul_vec ((hv₁.equiv_fun) v) j v₂ j

@[simp]
theorem matrix.to_lin_self {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) (M : matrix m n R) (i : n) :
((matrix.to_lin hv₁ hv₂) M) (v₁ i) = ∑ (j : m), M j i v₂ j

@[simp]
theorem linear_map.to_matrix_id {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_group M₁] [module R M₁] {v₁ : n → M₁} (hv₁ : is_basis R v₁) :

@[simp]
theorem matrix.to_lin_one {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_group M₁] [module R M₁] {v₁ : n → M₁} (hv₁ : is_basis R v₁) :

theorem linear_map.to_matrix_range {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) [decidable_eq M₁] [decidable_eq M₂] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
(linear_map.to_matrix _ _) f v₂ k, _⟩ v₁ i, _⟩ = (linear_map.to_matrix hv₁ hv₂) f k i

theorem linear_map.to_matrix_comp {R : Type u_1} [comm_ring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) {M₃ : Type u_7} [add_comm_group M₃] [module R M₃] {v₃ : l → M₃} (hv₃ : is_basis R v₃) [decidable_eq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
(linear_map.to_matrix hv₁ hv₃) (f.comp g) = (linear_map.to_matrix hv₂ hv₃) f (linear_map.to_matrix hv₁ hv₂) g

theorem linear_map.to_matrix_mul {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_group M₁] [module R M₁] {v₁ : n → M₁} (hv₁ : is_basis R v₁) (f g : M₁ →ₗ[R] M₁) :
(linear_map.to_matrix hv₁ hv₁) (f * g) = (linear_map.to_matrix hv₁ hv₁) f (linear_map.to_matrix hv₁ hv₁) g

theorem matrix.to_lin_mul {R : Type u_1} [comm_ring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype l] [fintype m] [fintype n] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] {v₁ : n → M₁} (hv₁ : is_basis R v₁) {v₂ : m → M₂} (hv₂ : is_basis R v₂) {M₃ : Type u_7} [add_comm_group M₃] [module R M₃] {v₃ : l → M₃} (hv₃ : is_basis R v₃) [decidable_eq m] (A : matrix l m R) (B : matrix m n R) :
(matrix.to_lin hv₁ hv₃) (A B) = ((matrix.to_lin hv₂ hv₃) A).comp ((matrix.to_lin hv₁ hv₂) B)

def is_basis.to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} :
is_basis R e(ι' → M)matrix ι ι' R

From a basis e : ι → M and a family of vectors v : ι' → M, make the matrix whose columns are the vectors v i written in the basis e.

Equations
theorem is_basis.to_matrix_apply {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι' → M) (i : ι) (j : ι') :
he.to_matrix v i j = (he.equiv_fun) (v j) i

theorem is_basis.to_matrix_eq_to_matrix_constr {ι : Type u_1} [fintype ι] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) [decidable_eq ι] (v : ι → M) :

@[simp]
theorem is_basis.to_matrix_self {ι : Type u_1} [fintype ι] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) [decidable_eq ι] :
he.to_matrix e = 1

theorem is_basis.to_matrix_update {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι' → M) (j : ι') [decidable_eq ι'] (x : M) :

@[simp]
theorem is_basis.sum_to_matrix_smul_self {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι' → M) (j : ι') :
∑ (i : ι), he.to_matrix v i j e i = v j

@[simp]
theorem is_basis.to_lin_to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι' → M) [decidable_eq ι'] (hv : is_basis R v) :

def is_basis.to_matrix_equiv {ι : Type u_1} [fintype ι] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} :
is_basis R e((ι → M) ≃ₗ[R] matrix ι ι R)

From a basis e : ι → M, build a linear equivalence between families of vectors v : ι → M, and matrices, making the matrix whose columns are the vectors v i written in the basis e.

Equations
@[simp]
theorem is_basis_to_matrix_mul_linear_map_to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {N : Type u_5} [add_comm_group N] [module R N] {b' : ι' → M} {c : ι → N} {c' : ι' → N} (hb' : is_basis R b') (hc : is_basis R c) (hc' : is_basis R c') (f : M →ₗ[R] N) [decidable_eq ι'] :

@[simp]
theorem linear_map_to_matrix_mul_is_basis_to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {N : Type u_5} [add_comm_group N] [module R N] {b : ι → M} {b' : ι' → M} {c' : ι' → N} (hb : is_basis R b) (hb' : is_basis R b') (hc' : is_basis R c') (f : M →ₗ[R] N) [decidable_eq ι] [decidable_eq ι'] :

theorem linear_equiv.is_unit_det {R : Type} [comm_ring R] {M : Type u_1} [add_comm_group M] [module R M] {M' : Type u_2} [add_comm_group M'] [module R M'] {ι : Type u_3} [decidable_eq ι] [fintype ι] {v : ι → M} {v' : ι → M'} (f : M ≃ₗ[R] M') (hv : is_basis R v) (hv' : is_basis R v') :

def linear_equiv.of_is_unit_det {R : Type} [comm_ring R] {M : Type u_1} [add_comm_group M] [module R M] {M' : Type u_2} [add_comm_group M'] [module R M'] {ι : Type u_3} [decidable_eq ι] [fintype ι] {v : ι → M} {v' : ι → M'} {f : M →ₗ[R] M'} {hv : is_basis R v} {hv' : is_basis R v'} :
is_unit ((linear_map.to_matrix hv hv') f).det(M ≃ₗ[R] M')

Builds a linear equivalence from a linear map whose determinant in some bases is a unit.

Equations
def is_basis.det {R : Type} [comm_ring R] {M : Type u_1} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] {e : ι → M} :
is_basis R emultilinear_map R (λ (i : ι), M) R

The determinant of a family of vectors with respect to some basis, as a multilinear map.

Equations
theorem is_basis.det_apply {R : Type} [comm_ring R] {M : Type u_1} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] {e : ι → M} (he : is_basis R e) (v : ι → M) :
(he.det) v = (he.to_matrix v).det

theorem is_basis.det_self {R : Type} [comm_ring R] {M : Type u_1} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] {e : ι → M} (he : is_basis R e) :
(he.det) e = 1

theorem is_basis.iff_det {R : Type} [comm_ring R] {M : Type u_1} [add_comm_group M] [module R M] {ι : Type u_3} [decidable_eq ι] [fintype ι] {e : ι → M} (he : is_basis R e) {v : ι → M} :
is_basis R v is_unit ((he.det) v)

@[simp]
theorem linear_map.to_matrix_transpose {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [field K] [add_comm_group V₁] [vector_space K V₁] [add_comm_group V₂] [vector_space K V₂] [fintype ι₁] [fintype ι₂] [decidable_eq ι₁] [decidable_eq ι₂] {B₁ : ι₁ → V₁} (h₁ : is_basis K B₁) {B₂ : ι₂ → V₂} (h₂ : is_basis K B₂) (u : V₁ →ₗ[K] V₂) :

theorem linear_map.to_matrix_symm_transpose {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [field K] [add_comm_group V₁] [vector_space K V₁] [add_comm_group V₂] [vector_space K V₂] [fintype ι₁] [fintype ι₂] [decidable_eq ι₁] [decidable_eq ι₂] {B₁ : ι₁ → V₁} (h₁ : is_basis K B₁) {B₂ : ι₂ → V₂} (h₂ : is_basis K B₂) (M : matrix ι₁ ι₂ K) :

def matrix.diag (n : Type u_2) [fintype n] (R : Type v) (M : Type w) [semiring R] [add_comm_monoid M] [semimodule R M] :
matrix n n M →ₗ[R] n → M

The diagonal of a square matrix.

Equations
@[simp]
theorem matrix.diag_apply {n : Type u_2} [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_2} [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_2} [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 = (matrix.diag n R M) A

def matrix.trace (n : Type u_2) [fintype n] (R : Type v) (M : Type w) [semiring R] [add_comm_monoid M] [semimodule R M] :
matrix n n M →ₗ[R] M

The trace of a square matrix.

Equations
@[simp]
theorem matrix.trace_diag {n : Type u_2} [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 = ∑ (i : n), (matrix.diag n R M) A i

@[simp]
theorem matrix.trace_one {n : Type u_2} [fintype n] {R : Type v} [semiring R] [decidable_eq n] :

@[simp]
theorem matrix.trace_transpose {n : Type u_2} [fintype n] {R : Type v} {M : Type w} [semiring R] [add_comm_monoid M] [semimodule R M] (A : matrix n n M) :

@[simp]
theorem matrix.trace_transpose_mul {m : Type u_1} [fintype m] {n : Type u_2} [fintype n] {R : Type v} [semiring R] (A : matrix m n R) (B : matrix n m R) :
(matrix.trace n R R) (A B) = (matrix.trace m R R) (A B)

theorem matrix.trace_mul_comm {m : Type u_1} [fintype m] {n : Type u_2} [fintype n] {S : Type v} [comm_ring S] (A : matrix m n S) (B : matrix n m S) :
(matrix.trace n S S) (B A) = (matrix.trace m S S) (A B)

theorem matrix.proj_diagonal {n : Type u_1} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] (i : n) (w : n → R) :

theorem matrix.diagonal_comp_std_basis {n : Type u_1} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] (w : n → R) (i : n) :
(matrix.to_lin' (matrix.diagonal w)).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_1} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] (w : n → R) :

def matrix.to_linear_equiv {n : Type u_1} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] (P : matrix n n R) :
is_unit P((n → R) ≃ₗ[R] n → R)

An invertible matrix yields a linear equivalence from the free module to itself.

Equations
@[simp]
theorem matrix.to_linear_equiv_apply {n : Type u_1} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] (P : matrix n n R) (h : is_unit P) :

@[simp]
theorem matrix.to_linear_equiv_symm_apply {n : Type u_1} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R] (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] [decidable_eq n] (w : m → K) (v : n → K) :

theorem matrix.ker_diagonal_to_lin' {m : Type u_1} [fintype m] {K : Type u} [field K] [decidable_eq m] (w : m → K) :
(matrix.to_lin' (matrix.diagonal w)).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_1} [fintype m] {K : Type u} [field K] [decidable_eq m] (w : m → K) :
(matrix.to_lin' (matrix.diagonal w)).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_1} [fintype m] {K : Type u} [field K] [decidable_eq m] [decidable_eq K] (w : m → K) :

@[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.findim_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.

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} :
m m'n n'matrix m n R matrix m' n' R

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Equations
@[simp]
theorem matrix.reindex_apply {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} (eₘ : m m') (eₙ : n n') (M : matrix m n R) :
(matrix.reindex eₘ eₙ) M = λ (i : m') (j : n'), M ((eₘ.symm) i) ((eₙ.symm) j)

@[simp]
theorem matrix.reindex_symm_apply {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} (eₘ : m m') (eₙ : n n') (M : matrix m' n' R) :
((matrix.reindex eₘ eₙ).symm) M = λ (i : m) (j : n), M (eₘ i) (eₙ j)

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] :
m m'n n'(matrix m n R ≃ₗ[R] matrix m' n' R)

The natural map that reindexes a matrix's rows and columns with equivalent types is a linear equivalence.

Equations
@[simp]
theorem matrix.reindex_linear_equiv_apply {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] (eₘ : m m') (eₙ : n n') (M : matrix m n R) :
(matrix.reindex_linear_equiv eₘ eₙ) M = λ (i : m') (j : n'), M ((eₘ.symm) i) ((eₙ.symm) j)

@[simp]
theorem matrix.reindex_linear_equiv_symm_apply {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] (eₘ : m m') (eₙ : n n') (M : matrix m' n' R) :
((matrix.reindex_linear_equiv eₘ eₙ).symm) M = λ (i : m) (j : n), M (eₘ i) (eₙ j)

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) :

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] :
m n(matrix m m R ≃ₐ[R] matrix n n R)

For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence of algebras.

Equations
@[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) :
(matrix.reindex_alg_equiv e) M = λ (i j : n), M ((e.symm) i) ((e.symm) j)

@[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) :
((matrix.reindex_alg_equiv e).symm) M = λ (i j : m), M (e i) (e j)

theorem matrix.reindex_transpose {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} (eₘ : m m') (eₙ : n n') (M : matrix m n R) :
((matrix.reindex eₘ eₙ) M) = (matrix.reindex eₙ eₘ) M

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} :
is_basis R b((M →ₗ[R] M) →ₗ[R] R)

The trace of an endomorphism given a basis.

Equations
@[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) :

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) :

theorem linear_map.trace_aux_range (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) :

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) :

where ι and κ can reside in different universes

def linear_map.trace (R : Type u) [comm_ring R] (M : Type v) [add_comm_group M] [module R M] :
(M →ₗ[R] M) →ₗ[R] R

Trace of an endomorphism independent of basis.

Equations
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 ι] [decidable_eq ι] {b : ι → M} (hb : is_basis R b) (f : M →ₗ[R] M) :

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)

@[instance]
def linear_map.finite_dimensional {K : Type u_1} [field K] {V : Type u_2} [add_comm_group V] [vector_space K V] [finite_dimensional K V] {W : Type u_3} [add_comm_group W] [vector_space K W] [finite_dimensional K W] :

@[simp]

The dimension of the space of linear transformations is the product of the dimensions of the domain and codomain.

def alg_equiv_matrix' {R : Type v} [comm_ring R] {n : Type u_1} [fintype n] [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
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.

Equations
def alg_equiv_matrix {R : Type v} {M : Type w} {n : Type u_1} [fintype n] [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.

Equations