# mathlib3documentation

linear_algebra.matrix.to_lin

# Linear maps and matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

• `linear_map.to_matrix`: given bases `v₁ : ι → M₁` and `v₂ : κ → M₂`, the `R`-linear equivalence from `M₁ →ₗ[R] M₂` to `matrix κ ι R`
• `matrix.to_lin`: the inverse of `linear_map.to_matrix`
• `linear_map.to_matrix'`: the `R`-linear equivalence from `(m → R) →ₗ[R] (n → R)` to `matrix m n R` (with the standard basis on `m → R` and `n → R`)
• `matrix.to_lin'`: the inverse of `linear_map.to_matrix'`
• `alg_equiv_matrix`: given a basis indexed by `n`, the `R`-algebra equivalence between `R`-endomorphisms of `M` and `matrix n n R`

## Issues #

This file was originally written without attention to non-commutative rings, and so mostly only works in the commutative setting. This should be fixed.

In particular, `matrix.mul_vec` gives us a linear equivalence `matrix m n R ≃ₗ[R] (n → R) →ₗ[Rᵐᵒᵖ] (m → R)` while `matrix.vec_mul` gives us a linear equivalence `matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] (n → R)`. At present, the first equivalence is developed in detail but only for commutative rings (and we omit the distinction between `Rᵐᵒᵖ` and `R`), while the second equivalence is developed only in brief, but for not-necessarily-commutative rings.

Naming is slightly inconsistent between the two developments. In the original (commutative) development `linear` is abbreviated to `lin`, although this is not consistent with the rest of mathlib. In the new (non-commutative) development `linear` is not abbreviated, and declarations use `_right` to indicate they use the right action of matrices on vectors (via `matrix.vec_mul`). When the two developments are made uniform, the names should be made uniform, too, by choosing between `linear` and `lin` consistently, and (presumably) adding `_left` where necessary.

## Tags #

linear_map, matrix, linear_equiv, diagonal, det, trace

@[protected, instance]
def matrix.fintype {n : Type u_1} {m : Type u_2} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] (R : Type u_3) [fintype R] :
fintype (matrix m n R)
Equations
def matrix.vec_mul_linear {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] (M : n R) :
(m R) →ₗ[R] n R

`matrix.vec_mul M` is a linear map.

Equations
@[simp]
theorem matrix.vec_mul_linear_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] (M : n R) (x : m R) (ᾰ : n) :
(M.vec_mul_linear) x =
@[simp]
theorem matrix.vec_mul_std_basis {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] (M : n R) (i : m) (j : n) :
matrix.vec_mul ( (λ (_x : m), R) i) 1) M j = M i j
def linear_map.to_matrix_right' {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] :
((m R) →ₗ[R] n R) ≃ₗ[Rᵐᵒᵖ] n R

Linear maps `(m → R) →ₗ[R] (n → R)` are linearly equivalent over `Rᵐᵒᵖ` to `matrix m n R`, by having matrices act by right multiplication.

Equations
@[reducible]
def matrix.to_linear_map_right' {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] :

A `matrix m n R` is linearly equivalent over `Rᵐᵒᵖ` to a linear map `(m → R) →ₗ[R] (n → R)`, by having matrices act by right multiplication.

@[simp]
theorem matrix.to_linear_map_right'_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] (M : n R) (v : m R) :
@[simp]
theorem matrix.to_linear_map_right'_mul {R : Type u_1} [semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype l] [decidable_eq l] (M : m R) (N : n R) :
theorem matrix.to_linear_map_right'_mul_apply {R : Type u_1} [semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype l] [decidable_eq l] (M : m R) (N : n R) (x : l R) :
@[simp]
theorem matrix.to_linear_map_right'_one {R : Type u_1} [semiring R] {m : Type u_3} [fintype m] [decidable_eq m] :
@[simp]
theorem matrix.to_linear_equiv_right'_of_inv_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : n R) (ᾰ_1 : m) :
hM'M) ᾰ_1 = ᾰ_1
def matrix.to_linear_equiv_right'_of_inv {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :
(n R) ≃ₗ[R] m R

If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `n → A` and `m → A` corresponding to `M.vec_mul` and `M'.vec_mul`.

Equations
@[simp]
theorem matrix.to_linear_equiv_right'_of_inv_symm_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : m R) (ᾰ_1 : n) :
hM'M).symm) ᾰ_1 = ᾰ_1

From this point on, we only work with commutative rings, and fail to distinguish between `Rᵐᵒᵖ` and `R`. This should eventually be remedied.

def matrix.mul_vec_lin {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] (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} {m : Type u_4} {n : Type u_5} [fintype n] (M : n R) (v : n R) :
@[simp]
theorem matrix.mul_vec_lin_zero {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] :
@[simp]
theorem matrix.mul_vec_lin_add {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] (M N : n R) :
(M + N).mul_vec_lin =
theorem matrix.mul_vec_lin_submatrix {R : Type u_1} {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [fintype l] (f₁ : m k) (e₂ : n l) (M : l R) :
(M.submatrix f₁ e₂).mul_vec_lin = f₁).comp (M.mul_vec_lin.comp (e₂.symm)))
theorem matrix.mul_vec_lin_reindex {R : Type u_1} {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [fintype l] (e₁ : k m) (e₂ : l n) (M : l R) :
( e₂) M).mul_vec_lin = e₁.symm).comp (M.mul_vec_lin.comp e₂))

A variant of `matrix.mul_vec_lin_submatrix` that keeps around `linear_equiv`s.

@[simp]
theorem matrix.mul_vec_lin_one {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.mul_vec_lin_mul {R : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [fintype m] (M : m R) (N : n R) :
theorem matrix.ker_mul_vec_lin_eq_bot_iff {R : Type u_1} {n : Type u_5} [fintype n] {M : n R} :
(v : n R), M.mul_vec v = 0 v = 0
theorem matrix.mul_vec_std_basis {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) (i : m) (j : n) :
M.mul_vec ( (λ (_x : n), R) j) 1) i = M i j
@[simp]
theorem matrix.mul_vec_std_basis_apply {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) (j : n) :
M.mul_vec ( (λ (_x : n), R) j) 1) = M.transpose j
theorem matrix.range_mul_vec_lin {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] (M : n R) :
def linear_map.to_matrix' {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] :
((n R) →ₗ[R] m R) ≃ₗ[R] 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} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] :
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)`.

Note that the forward-direction does not require `decidable_eq` and is `matrix.vec_mul_lin`.

Equations
theorem matrix.to_lin'_apply' {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) :
@[simp]
theorem linear_map.to_matrix'_symm {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_lin'_symm {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem linear_map.to_matrix'_to_lin' {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) :
@[simp]
theorem matrix.to_lin'_to_matrix' {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (f : (n R) →ₗ[R] m R) :
@[simp]
theorem linear_map.to_matrix'_apply {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (f : (n R) →ₗ[R] m R) (i : m) (j : n) :
= f (λ (j' : n), ite (j' = j) 1 0) i
@[simp]
theorem matrix.to_lin'_apply {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) (v : n R) :
v = M.mul_vec v
@[simp]
theorem matrix.to_lin'_one {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem linear_map.to_matrix'_id {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_lin'_mul {R : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype m] [decidable_eq m] (M : m R) (N : n R) :
@[simp]
theorem matrix.to_lin'_submatrix {R : Type u_1} {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype l] [decidable_eq l] (f₁ : m k) (e₂ : n l) (M : l R) :
theorem matrix.to_lin'_reindex {R : Type u_1} {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype l] [decidable_eq l] (e₁ : k m) (e₂ : l n) (M : l R) :

A variant of `matrix.to_lin'_submatrix` that keeps around `linear_equiv`s.

theorem matrix.to_lin'_mul_apply {R : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype m] [decidable_eq m] (M : m R) (N : n R) (x : n R) :

Shortcut lemma for `matrix.to_lin'_mul` and `linear_map.comp_apply`

theorem linear_map.to_matrix'_comp {R : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype l] [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} {m : Type u_4} [fintype m] [decidable_eq m] (f g : (m R) →ₗ[R] m R) :
@[simp]
theorem linear_map.to_matrix'_algebra_map {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (x : R) :
theorem matrix.ker_to_lin'_eq_bot_iff {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] {M : n R} :
(v : n R), M.mul_vec v = 0 v = 0
theorem matrix.range_to_lin' {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) :
@[simp]
theorem matrix.to_lin'_of_inv_symm_apply {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype m] [decidable_eq m] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : n R) (ᾰ_1 : m) :
((matrix.to_lin'_of_inv hMM' hM'M).symm) ᾰ_1 = ᾰ_1
def matrix.to_lin'_of_inv {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype m] [decidable_eq m] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :
(m R) ≃ₗ[R] n R

If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `m → A` and `n → A` corresponding to `M.mul_vec` and `M'.mul_vec`.

Equations
@[simp]
theorem matrix.to_lin'_of_inv_apply {R : Type u_1} {m : Type u_4} {n : Type u_5} [fintype n] [decidable_eq n] [fintype m] [decidable_eq m] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : m R) (ᾰ_1 : n) :
hM'M) ᾰ_1 = (matrix.to_lin' M') ᾰ_1
def linear_map.to_matrix_alg_equiv' {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
((n R) →ₗ[R] n R) ≃ₐ[R] 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} {n : Type u_5} [fintype n] [decidable_eq 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]
theorem linear_map.to_matrix_alg_equiv'_symm {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_lin_alg_equiv'_symm {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem linear_map.to_matrix_alg_equiv'_to_lin_alg_equiv' {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) :
@[simp]
theorem matrix.to_lin_alg_equiv'_to_matrix_alg_equiv' {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (f : (n R) →ₗ[R] n R) :
@[simp]
theorem linear_map.to_matrix_alg_equiv'_apply {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (f : (n R) →ₗ[R] n R) (i j : n) :
= f (λ (j' : n), ite (j' = j) 1 0) i
@[simp]
theorem matrix.to_lin_alg_equiv'_apply {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (M : n R) (v : n R) :
= M.mul_vec v
@[simp]
theorem matrix.to_lin_alg_equiv'_one {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem linear_map.to_matrix_alg_equiv'_id {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_lin_alg_equiv'_mul {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (M N : n R) :
theorem linear_map.to_matrix_alg_equiv'_comp {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (f g : (n R) →ₗ[R] n R) :
theorem linear_map.to_matrix_alg_equiv'_mul {R : Type u_1} {n : Type u_5} [fintype n] [decidable_eq n] (f g : (n R) →ₗ[R] n R) :
noncomputable def linear_map.to_matrix {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) :
(M₁ →ₗ[R] M₂) ≃ₗ[R] 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
theorem linear_map.to_matrix_eq_to_matrix' {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] :

`linear_map.to_matrix'` is a particular case of `linear_map.to_matrix`, for the standard basis `pi.basis_fun R n`.

noncomputable def matrix.to_lin {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R 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
theorem matrix.to_lin_eq_to_lin' {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] :

`matrix.to_lin'` is a particular case of `matrix.to_lin`, for the standard basis `pi.basis_fun R n`.

@[simp]
theorem linear_map.to_matrix_symm {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) :
v₂).symm = v₂
@[simp]
theorem matrix.to_lin_symm {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) :
v₂).symm = v₂
@[simp]
theorem matrix.to_lin_to_matrix {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (f : M₁ →ₗ[R] M₂) :
v₂) ( v₂) f) = f
@[simp]
theorem linear_map.to_matrix_to_lin {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (M : n R) :
v₂) ( v₂) M) = M
theorem linear_map.to_matrix_apply {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
v₂) f i j = ((v₂.repr) (f (v₁ j))) i
theorem linear_map.to_matrix_transpose_apply {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (f : M₁ →ₗ[R] M₂) (j : n) :
( v₂) f).transpose j = ((v₂.repr) (f (v₁ j)))
theorem linear_map.to_matrix_apply' {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
v₂) f i j = ((v₂.repr) (f (v₁ j))) i
theorem linear_map.to_matrix_transpose_apply' {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (f : M₁ →ₗ[R] M₂) (j : n) :
( v₂) f).transpose j = ((v₂.repr) (f (v₁ j)))
theorem matrix.to_lin_apply {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (M : n R) (v : M₁) :
( v₂) M) v = finset.univ.sum (λ (j : m), M.mul_vec ((v₁.repr) v) j v₂ j)
@[simp]
theorem matrix.to_lin_self {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (M : n R) (i : n) :
( v₂) M) (v₁ i) = finset.univ.sum (λ (j : m), M j i v₂ j)
theorem linear_map.to_matrix_id {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
= 1

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} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
v₁) 1 = 1
@[simp]
theorem matrix.to_lin_one {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
theorem linear_map.to_matrix_reindex_range {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) [decidable_eq M₁] [decidable_eq M₂] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
v₂ k, _⟩ v₁ i, _⟩ = v₂) f k i
theorem linear_map.to_matrix_comp {R : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) {M₃ : Type u_7} [add_comm_monoid M₃] [ M₃] (v₃ : R M₃) [fintype l] [decidable_eq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
v₃) (f.comp g) = ( v₃) f).mul ( v₂) g)
theorem linear_map.to_matrix_mul {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f g : M₁ →ₗ[R] M₁) :
v₁) (f * g) = ( v₁) f).mul ( v₁) g)
@[simp]
theorem linear_map.to_matrix_algebra_map {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (x : R) :
v₁) ( M₁)) x) = x
theorem linear_map.to_matrix_mul_vec_repr {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) (f : M₁ →ₗ[R] M₂) (x : M₁) :
( v₂) f).mul_vec ((v₁.repr) x) = ((v₂.repr) (f x))
@[simp]
theorem linear_map.to_matrix_basis_equiv {R : Type u_1} {l : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] [fintype l] [decidable_eq l] (b : R M₁) (b' : R M₂) :
b) (b'.equiv b (equiv.refl l)) = 1
theorem matrix.to_lin_mul {R : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) {M₃ : Type u_7} [add_comm_monoid M₃] [ M₃] (v₃ : R M₃) [fintype l] [decidable_eq m] (A : m R) (B : n R) :
v₃) (A.mul B) = ( v₃) A).comp ( v₂) B)
theorem matrix.to_lin_mul_apply {R : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) {M₃ : Type u_7} [add_comm_monoid M₃] [ M₃] (v₃ : R M₃) [fintype l] [decidable_eq m] (A : m R) (B : n R) (x : M₁) :
( v₃) (A.mul B)) x = ( v₃) A) (( v₂) B) x)

Shortcut lemma for `matrix.to_lin_mul` and `linear_map.comp_apply`.

@[simp]
theorem matrix.to_lin_of_inv_symm_apply {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) [decidable_eq m] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : M₂) :
v₂ hMM' hM'M).symm) = ( v₁) M')
noncomputable def matrix.to_lin_of_inv {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) [decidable_eq m] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :
M₁ ≃ₗ[R] M₂

If `M` and `M` are each other's inverse matrices, `matrix.to_lin M` and `matrix.to_lin M'` form a linear equivalence.

Equations
@[simp]
theorem matrix.to_lin_of_inv_apply {R : Type u_1} {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (v₁ : R M₁) (v₂ : R M₂) [decidable_eq m] {M : n R} {M' : m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : M₁) :
v₂ hMM' hM'M) = ( v₂) M)
noncomputable def linear_map.to_matrix_alg_equiv {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
(M₁ →ₗ[R] M₁) ≃ₐ[R] 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
noncomputable def matrix.to_lin_alg_equiv {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
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} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
@[simp]
theorem matrix.to_lin_alg_equiv_symm {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
@[simp]
theorem matrix.to_lin_alg_equiv_to_matrix_alg_equiv {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f : M₁ →ₗ[R] M₁) :
f) = f
@[simp]
theorem linear_map.to_matrix_alg_equiv_to_lin_alg_equiv {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (M : n R) :
( M) = M
theorem linear_map.to_matrix_alg_equiv_apply {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f : M₁ →ₗ[R] M₁) (i j : n) :
i j = ((v₁.repr) (f (v₁ j))) i
theorem linear_map.to_matrix_alg_equiv_transpose_apply {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f : M₁ →ₗ[R] M₁) (j : n) :
f).transpose j = ((v₁.repr) (f (v₁ j)))
theorem linear_map.to_matrix_alg_equiv_apply' {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f : M₁ →ₗ[R] M₁) (i j : n) :
i j = ((v₁.repr) (f (v₁ j))) i
theorem linear_map.to_matrix_alg_equiv_transpose_apply' {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f : M₁ →ₗ[R] M₁) (j : n) :
f).transpose j = ((v₁.repr) (f (v₁ j)))
theorem matrix.to_lin_alg_equiv_apply {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (M : n R) (v : M₁) :
( M) v = finset.univ.sum (λ (j : n), M.mul_vec ((v₁.repr) v) j v₁ j)
@[simp]
theorem matrix.to_lin_alg_equiv_self {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (M : n R) (i : n) :
( M) (v₁ i) = finset.univ.sum (λ (j : n), M j i v₁ j)
theorem linear_map.to_matrix_alg_equiv_id {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
@[simp]
theorem matrix.to_lin_alg_equiv_one {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) :
theorem linear_map.to_matrix_alg_equiv_reindex_range {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) [decidable_eq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
v₁ k, _⟩ v₁ i, _⟩ = k i
theorem linear_map.to_matrix_alg_equiv_comp {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f g : M₁ →ₗ[R] M₁) :
(f.comp g) = f).mul g)
theorem linear_map.to_matrix_alg_equiv_mul {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (f g : M₁ →ₗ[R] M₁) :
(f * g) = f).mul g)
theorem matrix.to_lin_alg_equiv_mul {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (A B : n R) :
(A.mul B) = ( A).comp ( B)
@[simp]
theorem matrix.to_lin_fin_two_prod_apply {R : Type u_1} (a b c d : R) (x : R × R) :
( (matrix.of ![![a, b], ![c, d]])) x = (a * x.fst + b * x.snd, c * x.fst + d * x.snd)
theorem matrix.to_lin_fin_two_prod {R : Type u_1} (a b c d : R) :
(matrix.of ![![a, b], ![c, d]]) = (a R + b R).prod (c R + d R)
@[simp]
theorem to_matrix_distrib_mul_action_to_linear_map {R : Type u_1} {n : Type u_4} [fintype n] [decidable_eq n] {M₁ : Type u_5} [add_comm_monoid M₁] [ M₁] (v₁ : R M₁) (x : R) :
v₁) x) = matrix.diagonal (λ (_x : n), x)
theorem algebra.to_matrix_lmul' {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) (x : S) (i j : m) :
b) ( S) x) i j = ((b.repr) (x * b j)) i
@[simp]
theorem algebra.to_matrix_lsmul {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) (x : R) :
b) ( S) x) = matrix.diagonal (λ (_x : m), x)
noncomputable def algebra.left_mul_matrix {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) :
S →ₐ[R] m R

`left_mul_matrix b 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 `linear_map.mul_left`, 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] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) (x : S) :
= b) ( S) x)
theorem algebra.left_mul_matrix_eq_repr_mul {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) (x : S) (i j : m) :
i j = ((b.repr) (x * b j)) i
theorem algebra.left_mul_matrix_mul_vec_repr {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) (x y : S) :
x).mul_vec ((b.repr) y) = ((b.repr) (x * y))
@[simp]
theorem algebra.to_matrix_lmul_eq {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) (x : S) :
b) x) =
theorem algebra.left_mul_matrix_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] [ S] {m : Type u_3} [fintype m] [decidable_eq m] (b : R S) :
theorem algebra.smul_left_mul_matrix {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [ring T] [ S] [ T] [ T] [ T] {m : Type u_4} {n : Type u_5} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (b : R S) (c : S T) (x : T) (ik jk : m × n) :
(algebra.left_mul_matrix (b.smul c)) x ik jk = x ik.snd jk.snd) ik.fst jk.fst
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] [ring T] [ S] [ T] [ T] [ T] {m : Type u_4} {n : Type u_5} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (b : R S) (c : S T) (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] [ring T] [ S] [ T] [ T] [ T] {m : Type u_4} {n : Type u_5} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (b : R S) (c : S T) (x : S) (i j : m) (k : n) :
(algebra.left_mul_matrix (b.smul c)) ( T) x) (i, k) (j, k) = i j
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] [ring T] [ S] [ T] [ T] [ T] {m : Type u_4} {n : Type u_5} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (b : R S) (c : S T) (x : S) (i j : m) {k k' : n} (h : k k') :
(algebra.left_mul_matrix (b.smul c)) ( T) x) (i, k) (j, k') = 0
def alg_equiv_matrix' {R : Type v} [comm_ring R] {n : Type u_1} [decidable_eq n] [fintype n] :
(n R) ≃ₐ[R] 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_3} {M₂ : Type u_4} [add_comm_group M₁] [ M₁] [add_comm_group M₂] [ M₂] (e : M₁ ≃ₗ[R] M₂) :
M₁ ≃ₐ[R] M₂

A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.

Equations
noncomputable def alg_equiv_matrix {R : Type v} [comm_ring R] {n : Type u_1} [decidable_eq n] {M : Type u_2} [ M] [fintype n] (h : R M) :
M ≃ₐ[R] n R

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

Equations