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

Some results are proved for determinants of block triangular matrices.

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] (M : 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_alg_equiv' {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] :
((n → R) →ₗ[R] n → R) ≃ₐ[R] matrix n n R

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

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

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

Equations
@[simp]
@[simp]
theorem linear_map.to_matrix_alg_equiv'_apply {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] (f : (n → R) →ₗ[R] n → R) (i j : n) :
linear_map.to_matrix_alg_equiv' f i j = f (λ (j' : n), ite (j' = j) 1 0) i
@[simp]
theorem matrix.to_lin_alg_equiv'_apply {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] (M : matrix n n R) (v : n → R) :
@[simp]
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₂} (hv₂ : 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₂} (hv₂ : 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_transpose_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₂) (j : n) :
((linear_map.to_matrix hv₁ hv₂) f) j = (hv₂.equiv_fun) (f (v₁ j))
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 linear_map.to_matrix_transpose_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₂) (j : n) :
((linear_map.to_matrix hv₁ hv₂) f) j = ((hv₂.repr) (f (v₁ j)))
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
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₁) :

This will be a special case of linear_map.to_matrix_id_eq_basis_to_matrix.

theorem linear_map.to_matrix_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₁) :
(linear_map.to_matrix hv₁ hv₁) 1 = 1
@[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 linear_map.to_matrix_mul_vec_repr {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₂) (x : M₁) :
((linear_map.to_matrix hv₁ hv₂) f).mul_vec ((hv₁.repr) x) = ((hv₂.repr) (f x))
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 linear_map.to_matrix_alg_equiv {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₁) :
(M₁ →ₗ[R] M₁) ≃ₐ[R] matrix n n R

Given a basis of a module M₁ over a commutative ring R, we get an algebra equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis.

Equations
def matrix.to_lin_alg_equiv {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₁) :
matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁

Given a basis of a module M₁ over a commutative ring R, we get an algebra equivalence between square matrices over R indexed by the basis and linear maps M₁ →ₗ M₁.

Equations
@[simp]
theorem linear_map.to_matrix_alg_equiv_symm {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_alg_equiv_symm {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_alg_equiv_to_matrix_alg_equiv {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 : M₁ →ₗ[R] M₁) :
@[simp]
theorem linear_map.to_matrix_alg_equiv_to_lin_alg_equiv {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₁) (M : matrix n n R) :
theorem linear_map.to_matrix_alg_equiv_apply {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 : M₁ →ₗ[R] M₁) (i j : n) :
(linear_map.to_matrix_alg_equiv hv₁) f i j = (hv₁.equiv_fun) (f (v₁ j)) i
theorem linear_map.to_matrix_alg_equiv_transpose_apply {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 : M₁ →ₗ[R] M₁) (j : n) :
((linear_map.to_matrix_alg_equiv hv₁) f) j = (hv₁.equiv_fun) (f (v₁ j))
theorem linear_map.to_matrix_alg_equiv_apply' {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 : M₁ →ₗ[R] M₁) (i j : n) :
(linear_map.to_matrix_alg_equiv hv₁) f i j = ((hv₁.repr) (f (v₁ j))) i
theorem linear_map.to_matrix_alg_equiv_transpose_apply' {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 : M₁ →ₗ[R] M₁) (j : n) :
((linear_map.to_matrix_alg_equiv hv₁) f) j = ((hv₁.repr) (f (v₁ j)))
theorem matrix.to_lin_alg_equiv_apply {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₁) (M : matrix n n R) (v : M₁) :
((matrix.to_lin_alg_equiv hv₁) M) v = ∑ (j : n), M.mul_vec ((hv₁.equiv_fun) v) j v₁ j
@[simp]
theorem matrix.to_lin_alg_equiv_self {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₁) (M : matrix n n R) (i : n) :
((matrix.to_lin_alg_equiv hv₁) M) (v₁ i) = ∑ (j : n), M j i v₁ j
theorem linear_map.to_matrix_alg_equiv_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_alg_equiv_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_alg_equiv_range {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₁) [decidable_eq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
theorem linear_map.to_matrix_alg_equiv_comp {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₁) :
theorem linear_map.to_matrix_alg_equiv_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₁) :
theorem matrix.to_lin_alg_equiv_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₁) (A B : matrix n n R) :
def is_basis.to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι' → 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_5} {M : Type u_6} [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_transpose_apply {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : is_basis R e) (v : ι' → M) (j : ι') :
(he.to_matrix v) j = ((he.repr) (v j))
theorem is_basis.to_matrix_eq_to_matrix_constr {ι : Type u_1} [fintype ι] {R : Type u_5} {M : Type u_6} [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_5} {M : Type u_6} [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_5} {M : Type u_6} [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_5} {M : Type u_6} [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_5} {M : Type u_6} [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_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {e : ι → M} (he : 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_2} {κ : Type u_3} {κ' : Type u_4} [fintype ι'] [fintype κ] [fintype κ'] {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {N : Type u_7} [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} {κ' : Type u_4} [fintype ι] [fintype ι'] [fintype κ'] {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {N : Type u_7} [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 ι'] :
@[simp]
theorem linear_map.to_matrix_id_eq_basis_to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {b : ι → M} {b' : ι' → M} (hb : is_basis R b) (hb' : is_basis R b') [decidable_eq ι] :

A generalization of linear_map.to_matrix_id.

@[simp]
theorem is_basis.to_matrix_mul_to_matrix {ι : Type u_1} {ι' : Type u_2} [fintype ι] [fintype ι'] {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] {b : ι → M} {b' : ι' → M} (hb : is_basis R b) (hb' : is_basis R b') {ι'' : Type u_3} [fintype ι''] {b'' : ι'' → M} (hb'' : is_basis R b'') :
hb.to_matrix b' hb'.to_matrix b'' = hb.to_matrix b''

A generalization of is_basis.to_matrix_self, in the opposite direction.

theorem linear_equiv.is_unit_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [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 u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {M' : Type u_3} [add_comm_group M'] [module R M'] {ι : Type u_4} [decidable_eq ι] [fintype ι] {v : ι → M} {v' : ι → M'} {f : M →ₗ[R] M'} {hv : is_basis R v} {hv' : is_basis R v'} (h : 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 u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {e : ι → M} (he : is_basis R e) :

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

Equations
theorem is_basis.det_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [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 u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [decidable_eq ι] [fintype ι] {e : ι → M} (he : is_basis R e) :
(he.det) e = 1
theorem is_basis.iff_det {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {ι : Type u_4} [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
theorem matrix.trace_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) :
(matrix.trace n R M) A = ∑ (i : n), A i 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) (h : is_unit P) :
(n → R) ≃ₗ[R] n → R

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

See matrix.to_linear_equiv for the same map on arbitrary modules.

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) :
@[simp]
theorem matrix.to_linear_equiv_apply {n : Type u_2} [fintype n] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {b : n → M} (hb : is_basis R b) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) (ᾰ : M) :
(matrix.to_linear_equiv hb A hA) = ((matrix.to_lin hb hb) A)
def matrix.to_linear_equiv {n : Type u_2} [fintype n] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {b : n → M} (hb : is_basis R b) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :

Given hA : is_unit A.det and hb : is_basis R b, A.to_linear_equiv hb hA is the linear_equiv arising from to_lin hb hb A.

See matrix.to_linear_equiv' for this result on n → R.

Equations
theorem matrix.ker_to_lin_eq_bot {n : Type u_2} [fintype n] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {b : n → M} (hb : is_basis R b) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
theorem matrix.range_to_lin_eq_top {n : Type u_2} [fintype n] {R : Type u_3} {M : Type u_4} [comm_ring R] [add_comm_group M] [module R M] {b : n → M} (hb : is_basis R b) [decidable_eq n] (A : matrix n n R) (hA : is_unit A.det) :
@[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_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] (eₘ : m m') (eₙ : 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, matrix.reindex, 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) :
@[simp]
theorem matrix.reindex_linear_equiv_symm {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') :
@[simp]
theorem matrix.reindex_linear_equiv_refl_refl {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type v} [semiring 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] (e : 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, matrix.reindex, 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) :
@[simp]
theorem matrix.reindex_alg_equiv_symm {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) :
theorem matrix.det_reindex_linear_equiv_self {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type v} [decidable_eq m] [decidable_eq n] [comm_ring R] (e : m n) (A : matrix m m R) :

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_minor_equiv_self.

theorem matrix.det_reindex_alg_equiv {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {R : Type v} [decidable_eq m] [decidable_eq n] [comm_ring R] (e : m n) (A : matrix m m R) :

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_minor_equiv_self.

theorem algebra.to_matrix_lmul' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) (x : S) (i j : m) :
(linear_map.to_matrix hb hb) ((algebra.lmul R S) x) i j = ((hb.repr) (x * b j)) i
@[simp]
theorem algebra.to_matrix_lsmul {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) (x : R) (i j : m) :
(linear_map.to_matrix hb hb) ((algebra.lsmul R S) x) i j = ite (i = j) x 0
def algebra.left_mul_matrix {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) :
S →ₐ[R] matrix m m R

left_mul_matrix hb x is the matrix corresponding to the linear map λ y, x * y.

left_mul_matrix_eq_repr_mul gives a formula for the entries of left_mul_matrix.

This definition is useful for doing (more) explicit computations with algebra.lmul, such as the trace form or norm map for algebras.

Equations
theorem algebra.left_mul_matrix_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) (x : S) :
theorem algebra.left_mul_matrix_eq_repr_mul {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) (x : S) (i j : m) :
(algebra.left_mul_matrix hb) x i j = ((hb.repr) (x * b j)) i
theorem algebra.left_mul_matrix_mul_vec_repr {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) (x y : S) :
@[simp]
theorem algebra.to_matrix_lmul_eq {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) (x : S) :
theorem algebra.left_mul_matrix_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] {m : Type u_4} [fintype m] [decidable_eq m] {b : m → S} (hb : is_basis R b) :
theorem algebra.smul_left_mul_matrix {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T] {m : Type u_4} {n : Type u_5} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {b : m → S} (hb : is_basis R b) {c : n → T} (hc : is_basis S c) (x : T) (i j : m) (k k' : n) :
theorem algebra.smul_left_mul_matrix_algebra_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T] {m : Type u_4} {n : Type u_5} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {b : m → S} (hb : is_basis R b) {c : n → T} (hc : is_basis S c) (x : S) :
theorem algebra.smul_left_mul_matrix_algebra_map_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T] {m : Type u_4} {n : Type u_5} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {b : m → S} (hb : is_basis R b) {c : n → T} (hc : is_basis S c) (x : S) (i j : m) (k : n) :
theorem algebra.smul_left_mul_matrix_algebra_map_ne {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] [algebra R S] [algebra S T] [algebra R T] [is_scalar_tower R S T] {m : Type u_4} {n : Type u_5} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {b : m → S} (hb : is_basis R b) {c : n → T} (hc : is_basis S c) (x : S) (i j : m) {k k' : n} (h : k k') :
(algebra.left_mul_matrix _) ((algebra_map S T) x) (i, k) (j, k') = 0
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} (hb : is_basis R b) :
(M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Equations
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₂] (e : M₁ ≃ₗ[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} (h : is_basis R b) :

A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.

Equations
@[simp]
theorem matrix.dot_product_std_basis_eq_mul {R : Type v} [semiring R] {n : Type w} [fintype n] [decidable_eq n] (v : n → R) (c : R) (i : n) :
matrix.dot_product v ((linear_map.std_basis R (λ (_x : n), R) i) c) = (v i) * c
@[simp]
theorem matrix.dot_product_std_basis_one {R : Type v} [semiring R] {n : Type w} [fintype n] [decidable_eq n] (v : n → R) (i : n) :
matrix.dot_product v ((linear_map.std_basis R (λ (_x : n), R) i) 1) = v i
theorem matrix.dot_product_eq {R : Type v} [semiring R] {n : Type w} [fintype n] (v w : n → R) (h : ∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) :
v = w
theorem matrix.dot_product_eq_iff {R : Type v} [semiring R] {n : Type w} [fintype n] {v w : n → R} :
(∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) v = w
theorem matrix.dot_product_eq_zero {R : Type v} [semiring R] {n : Type w} [fintype n] (v : n → R) (h : ∀ (w : n → R), matrix.dot_product v w = 0) :
v = 0
theorem matrix.dot_product_eq_zero_iff {R : Type v} [semiring R] {n : Type w} [fintype n] {v : n → R} :
(∀ (w : n → R), matrix.dot_product v w = 0) v = 0
theorem matrix.det_to_block {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (p : m → Prop) [decidable_pred p] :
M.det = ((M.to_block p p).from_blocks (M.to_block p (λ (j : m), ¬p j)) (M.to_block (λ (j : m), ¬p j) p) (M.to_block (λ (j : m), ¬p j) (λ (j : m), ¬p j))).det
theorem matrix.det_to_square_block {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {n : } (b : m → fin n) (k : fin n) :
(M.to_square_block b k).det = (M.to_square_block_prop (λ (i : m), b i = k)).det
theorem matrix.det_to_square_block' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (b : m → ) (k : ) :
(M.to_square_block' b k).det = (M.to_square_block_prop (λ (i : m), b i = k)).det
theorem matrix.two_block_triangular_det {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (p : m → Prop) [decidable_pred p] (h : ∀ (i : m), ¬p i∀ (j : m), p jM i j = 0) :
M.det = ((M.to_square_block_prop p).det) * (M.to_square_block_prop (λ (i : m), ¬p i)).det
theorem matrix.equiv_block_det {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {p q : m → Prop} [decidable_pred p] [decidable_pred q] (e : ∀ (x : m), q x p x) :
theorem matrix.to_square_block_det'' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {n : } (b : m → fin n) (k : fin n) :
(M.to_square_block b k).det = (M.to_square_block' (λ (i : m), (b i)) k).det
def matrix.block_triangular_matrix' {R : Type v} [comm_ring R] {o : Type u_1} [fintype o] (M : matrix o o R) {n : } (b : o → fin n) :
Prop

Let b map rows and columns of a square matrix M to n blocks. Then block_triangular_matrix' M n b says the matrix is block triangular.

Equations
theorem matrix.upper_two_block_triangular' {R : Type v} [comm_ring R] {m : Type u_1} {n : Type u_2} [fintype m] [fintype n] (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
(A.from_blocks B 0 D).block_triangular_matrix' (sum.elim (λ (i : m), 0) (λ (j : n), 1))
def matrix.block_triangular_matrix {R : Type v} [comm_ring R] {o : Type u_1} [fintype o] (M : matrix o o R) (b : o → ) :
Prop

Let b map rows and columns of a square matrix M to blocks indexed by s. Then block_triangular_matrix M n b says the matrix is block triangular.

Equations
theorem matrix.upper_two_block_triangular {R : Type v} [comm_ring R] {m : Type u_1} {n : Type u_2} [fintype m] [fintype n] (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
(A.from_blocks B 0 D).block_triangular_matrix (sum.elim (λ (i : m), 0) (λ (j : n), 1))
theorem matrix.det_of_block_triangular_matrix {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (b : m → ) (h : M.block_triangular_matrix b) (n : ) (hn : ∀ (i : m), b i < n) :
M.det = ∏ (k : ) in finset.range n, (M.to_square_block' b k).det
theorem matrix.det_of_block_triangular_matrix'' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (b : m → ) (h : M.block_triangular_matrix b) :
theorem matrix.det_of_block_triangular_matrix' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {n : } (b : m → fin n) (h : M.block_triangular_matrix' b) :
M.det = ∏ (k : fin n), (M.to_square_block b k).det
theorem matrix.det_of_upper_triangular {R : Type v} [comm_ring R] {n : } (M : matrix (fin n) (fin n) R) (h : ∀ (i j : fin n), j < iM i j = 0) :
M.det = ∏ (i : fin n), M i i
theorem matrix.det_of_lower_triangular {R : Type v} [comm_ring R] {n : } (M : matrix (fin n) (fin n) R) (h : ∀ (i j : fin n), i < jM i j = 0) :
M.det = ∏ (i : fin n), M i i