# mathlibdocumentation

linear_algebra.matrix.sesquilinear_form

# Sesquilinear form #

This file defines the conversion between sesquilinear forms and matrices.

## Main definitions #

• matrix.to_linear_map₂ given a basis define a bilinear form
• matrix.to_linear_map₂' define the bilinear form on n → R
• linear_map.to_matrix₂: calculate the matrix coefficients of a bilinear form
• linear_map.to_matrix₂': calculate the matrix coefficients of a bilinear form on n → R

## Todos #

At the moment this is quite a literal port from matrix.bilinear_form. Everything should be generalized to fully semibilinear forms.

## Tags #

sesquilinear_form, matrix, basis

def matrix.to_linear_map₂'_aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_semiring R₁] [comm_semiring R₂] [fintype n] [fintype m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (f : m R) :
(n R₁) →ₛₗ[σ₁] (m R₂) →ₛₗ[σ₂] R

The map from matrix n n R to bilinear forms on n → R.

This is an auxiliary definition for the equivalence matrix.to_linear_map₂'.

Equations
theorem matrix.to_linear_map₂'_aux_std_basis {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_semiring R₁] [comm_semiring R₂] [fintype n] [fintype m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) [decidable_eq n] [decidable_eq m] (f : m R) (i : n) (j : m) :
( f) ( (λ (_x : n), R₁) i) 1)) ( (λ (_x : m), R₂) j) 1) = f i j
def linear_map.to_matrix₂_aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_semiring R₁] [comm_semiring R₂] [add_comm_monoid M₁] [module R₁ M₁] [add_comm_monoid M₂] [module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (b₁ : n M₁) (b₂ : m M₂) :
(M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) →ₗ[R] m R

The linear map from sesquilinear forms to matrix n m R given an n-indexed basis for M₁ and an m-indexed basis for M₂.

This is an auxiliary definition for the equivalence matrix.to_linear_mapₛₗ₂'.

Equations
@[simp]
theorem linear_map.to_matrix₂_aux_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_semiring R₁] [comm_semiring R₂] [add_comm_monoid M₁] [module R₁ M₁] [add_comm_monoid M₂] [module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (b₁ : n M₁) (b₂ : m M₂) (i : n) (j : m) :
b₂) f i j = (f (b₁ i)) (b₂ j)
theorem linear_map.to_linear_map₂'_aux_to_matrix₂_aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : (n R₁) →ₛₗ[σ₁] (m R₂) →ₛₗ[σ₂] R) :
((linear_map.to_matrix₂_aux (λ (i : n), (λ (_x : n), R₁) i) 1) (λ (j : m), (λ (_x : m), R₂) j) 1)) f) = f
theorem matrix.to_matrix₂_aux_to_linear_map₂'_aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : m R) :
(linear_map.to_matrix₂_aux (λ (i : n), (λ (_x : n), R₁) i) 1) (λ (j : m), (λ (_x : m), R₂) j) 1)) f) = f

### Bilinear forms over n → R#

This section deals with the conversion between matrices and sesquilinear forms on n → R.

def linear_map.to_matrixₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} :
((n R₁) →ₛₗ[σ₁] (m R₂) →ₛₗ[σ₂] R) ≃ₗ[R] m R

The linear equivalence between sesquilinear forms and n × m matrices

Equations
def linear_map.to_matrix₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] :
((n R) →ₗ[R] (m R) →ₗ[R] R) ≃ₗ[R] m R

The linear equivalence between bilinear forms and n × m matrices

Equations
def matrix.to_linear_mapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
m R ≃ₗ[R] (n R₁) →ₛₗ[σ₁] (m R₂) →ₛₗ[σ₂] R

The linear equivalence between n × n matrices and sesquilinear forms on n → R

Equations
def matrix.to_linear_map₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] :
m R ≃ₗ[R] (n R) →ₗ[R] (m R) →ₗ[R] R

The linear equivalence between n × n matrices and bilinear forms on n → R

Equations
theorem matrix.to_linear_mapₛₗ₂'_aux_eq {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : m R) :
M = σ₂) M
theorem matrix.to_linear_mapₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : m R) (x : n R₁) (y : m R₂) :
(( σ₂) M) x) y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : m), σ₁ (x i) * M i j * σ₂ (y j)))
theorem matrix.to_linear_map₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (M : m R) (x : n R) (y : m R) :
x) y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : m), x i * M i j * y j))
theorem matrix.to_linear_map₂'_apply' {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (M : m R) (v : n R) (w : m R) :
v) w = (M.mul_vec w)
@[simp]
theorem matrix.to_linear_mapₛₗ₂'_std_basis {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : m R) (i : n) (j : m) :
(( σ₂) M) ( (λ (_x : n), R₁) i) 1)) ( (λ (_x : m), R₂) j) 1) = M i j
@[simp]
theorem matrix.to_linear_map₂'_std_basis {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (M : m R) (i : n) (j : m) :
( (λ (_x : n), R) i) 1)) ( (λ (_x : m), R) j) 1) = M i j
@[simp]
theorem linear_map.to_matrixₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
@[simp]
theorem matrix.to_linear_mapₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
@[simp]
theorem matrix.to_linear_mapₛₗ₂'_to_matrix' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (n R₁) →ₛₗ[σ₁] (m R₂) →ₛₗ[σ₂] R) :
= B
@[simp]
theorem matrix.to_linear_map₂'_to_matrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) :
@[simp]
theorem linear_map.to_matrix'_to_linear_mapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : m R) :
= M
@[simp]
theorem linear_map.to_matrix'_to_linear_map₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (M : m R) :
@[simp]
theorem linear_map.to_matrixₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [comm_ring R] [comm_ring R₁] [comm_ring R₂] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (n R₁) →ₛₗ[σ₁] (m R₂) →ₛₗ[σ₂] R) (i : n) (j : m) :
= (B ( (λ (_x : n), R₁) i) 1)) ( (λ (_x : m), R₂) j) 1)
@[simp]
theorem linear_map.to_matrix₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (i : n) (j : m) :
= (B ( (λ (_x : n), R) i) 1)) ( (λ (_x : m), R) j) 1)
@[simp]
theorem linear_map.to_matrix₂'_compl₁₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (l : (n' R) →ₗ[R] n R) (r : (m' R) →ₗ[R] m R) :
theorem linear_map.to_matrix₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype n'] [decidable_eq n'] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (f : (n' R) →ₗ[R] n R) :
theorem linear_map.to_matrix₂'_compl₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype m'] [decidable_eq m'] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (f : (m' R) →ₗ[R] m R) :
theorem linear_map.mul_to_matrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (M : matrix n' n R) (N : m' R) :
(M.mul .mul N =
theorem linear_map.mul_to_matrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype n'] [decidable_eq n'] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (M : matrix n' n R) :
theorem linear_map.to_matrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype m'] [decidable_eq m'] (B : (n R) →ₗ[R] (m R) →ₗ[R] R) (M : m' R) :
theorem matrix.to_linear_map₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [fintype n] [fintype m] [decidable_eq n] [decidable_eq m] [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (M : m R) (P : n' R) (Q : m' R) :

### Bilinear forms over arbitrary vector spaces #

This section deals with the conversion between matrices and bilinear forms on a module with a fixed basis.

noncomputable def linear_map.to_matrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) :
(M₁ →ₗ[R] M₂ →ₗ[R] R) ≃ₗ[R] m R

linear_map.to_matrix₂ b₁ b₂ is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if b is an R-basis for M.

Equations
noncomputable def matrix.to_linear_map₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) :
m R ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] R

bilin_form.to_matrix b is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if b is an R-basis for M.

Equations
@[simp]
theorem linear_map.to_matrix₂_apply {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (i : n) (j : m) :
b₂) B i j = (B (b₁ i)) (b₂ j)
@[simp]
theorem matrix.to_linear_map₂_apply {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) (M : m R) (x : M₁) (y : M₂) :
(( b₂) M) x) y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : m), ((b₁.repr) x) i * M i j * ((b₂.repr) y) j))
theorem linear_map.to_matrix₂_aux_eq {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
b₂) B = b₂) B
@[simp]
theorem linear_map.to_matrix₂_symm {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) :
b₂).symm =
@[simp]
theorem matrix.to_linear_map₂_symm {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) :
b₂).symm =
theorem matrix.to_linear_map₂_basis_fun {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] :
theorem linear_map.to_matrix₂_basis_fun {R : Type u_1} {n : Type u_9} {m : Type u_10} [comm_ring R] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] :
@[simp]
theorem matrix.to_linear_map₂_to_matrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
b₂) ( b₂) B) = B
@[simp]
theorem linear_map.to_matrix₂_to_linear_map₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) (M : m R) :
b₂) ( b₂) M) = M
theorem linear_map.to_matrix₂_compl₁₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₁'] [ M₁'] [add_comm_monoid M₂'] [ M₂'] (b₁' : basis n' R M₁') (b₂' : basis m' R M₂') [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁) (r : M₂' →ₗ[R] M₂) :
b₂') (B.compl₁₂ l r) = (( b₁) l).transpose.mul ( b₂) B)).mul ( b₂) r)
theorem linear_map.to_matrix₂_comp {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₁'] [ M₁'] (b₁' : basis n' R M₁') [fintype n'] [decidable_eq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₁' →ₗ[R] M₁) :
b₂) (B.comp f) = ( b₁) f).transpose.mul ( b₂) B)
theorem linear_map.to_matrix₂_compl₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₂'] [ M₂'] (b₂' : basis m' R M₂') [fintype m'] [decidable_eq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₂' →ₗ[R] M₂) :
b₂') (B.compl₂ f) = ( b₂) B).mul ( b₂) f)
@[simp]
theorem linear_map.to_matrix₂_mul_basis_to_matrix {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (c₁ : basis n' R M₁) (c₂ : basis m' R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
((b₁.to_matrix c₁).transpose.mul ( b₂) B)).mul (b₂.to_matrix c₂) = c₂) B
theorem linear_map.mul_to_matrix₂_mul {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₁'] [ M₁'] [add_comm_monoid M₂'] [ M₂'] (b₁' : basis n' R M₁') (b₂' : basis m' R M₂') [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : matrix n' n R) (N : m' R) :
(M.mul ( b₂) B)).mul N = b₂') (B.compl₁₂ ((matrix.to_lin b₁' b₁) M.transpose) ((matrix.to_lin b₂' b₂) N))
theorem linear_map.mul_to_matrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₁'] [ M₁'] (b₁' : basis n' R M₁') [fintype n'] [decidable_eq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : matrix n' n R) :
M.mul ( b₂) B) = b₂) (B.comp ((matrix.to_lin b₁' b₁) M.transpose))
theorem linear_map.to_matrix₂_mul {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₂'] [ M₂'] (b₂' : basis m' R M₂') [fintype m'] [decidable_eq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : m' R) :
( b₂) B).mul M = b₂') (B.compl₂ ((matrix.to_lin b₂' b₂) M))
theorem matrix.to_linear_map₂_compl₁₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {M₁' : Type u_7} {M₂' : Type u_8} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] (b₁ : R M₁) (b₂ : R M₂) [add_comm_monoid M₁'] [ M₁'] [add_comm_monoid M₂'] [ M₂'] (b₁' : basis n' R M₁') (b₂' : basis m' R M₂') [fintype n'] [fintype m'] [decidable_eq n'] [decidable_eq m'] (M : m R) (P : n' R) (Q : m' R) :
( b₂) M).compl₁₂ ((matrix.to_lin b₁' b₁) P) ((matrix.to_lin b₂' b₂) Q) = b₂') ((P.transpose.mul M).mul Q)

def matrix.is_adjoint_pair {R : Type u_1} {n : Type u_9} {n' : Type u_11} [comm_ring R] [fintype n] [fintype n'] (J : n R) (J' : matrix n' n' R) (A : matrix n' n R) (A' : n' R) :
Prop

The condition for the matrices A, A' to be an adjoint pair with respect to the square matrices J, J₃.

Equations
def matrix.is_self_adjoint {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J A₁ : n R) :
Prop

The condition for a square matrix A to be self-adjoint with respect to the square matrix J.

Equations
def matrix.is_skew_adjoint {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J A₁ : n R) :
Prop

The condition for a square matrix A to be skew-adjoint with respect to the square matrix J.

Equations
@[simp]
theorem is_adjoint_pair_to_linear_map₂' {R : Type u_1} {n : Type u_9} {n' : Type u_11} [comm_ring R] [fintype n] [fintype n'] (J : n R) (J' : matrix n' n' R) (A : matrix n' n R) (A' : n' R) [decidable_eq n] [decidable_eq n'] :
@[simp]
theorem is_adjoint_pair_to_linear_map₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {n' : Type u_11} [comm_ring R] [add_comm_monoid M₁] [ M₁] [add_comm_monoid M₂] [ M₂] [fintype n] [fintype n'] (b₁ : R M₁) (b₂ : basis n' R M₂) (J : n R) (J' : matrix n' n' R) (A : matrix n' n R) (A' : n' R) [decidable_eq n] [decidable_eq n'] :
( b₁) J).is_adjoint_pair ( b₂) J') ( b₂) A) ( b₁) A') J.is_adjoint_pair J' A A'
theorem matrix.is_adjoint_pair_equiv {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J A₁ : n R) [decidable_eq n] (P : n R) (h : is_unit P) :
((P.transpose.mul J).mul P).is_adjoint_pair ((P.transpose.mul J).mul P) A₁ A₁ ((P.mul A₁).mul P⁻¹) ((P.mul A₁).mul P⁻¹)
def pair_self_adjoint_matrices_submodule {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J J₂ : n R) [decidable_eq n] :
(matrix n n R)

The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to given matrices J, J₂.

Equations
@[simp]
theorem mem_pair_self_adjoint_matrices_submodule {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J J₂ A₁ : n R) [decidable_eq n] :
def self_adjoint_matrices_submodule {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J : n R) [decidable_eq n] :
(matrix n n R)

The submodule of self-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations
@[simp]
theorem mem_self_adjoint_matrices_submodule {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J A₁ : n R) [decidable_eq n] :
def skew_adjoint_matrices_submodule {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J : n R) [decidable_eq n] :
(matrix n n R)

The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations
@[simp]
theorem mem_skew_adjoint_matrices_submodule {R : Type u_1} {n : Type u_9} [comm_ring R] [fintype n] (J A₁ : n R) [decidable_eq n] :

### Nondegenerate bilinear forms #

theorem matrix.separating_left_to_linear_map₂'_iff_separating_left_to_linear_map₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] {M : ι R₁} (b : R₁ M₁) :
theorem matrix.nondegenerate.to_linear_map₂' {R₁ : Type u_2} {ι : Type u_13} [comm_ring R₁] [decidable_eq ι] [fintype ι] {M : ι R₁} (h : M.nondegenerate) :
@[simp]
theorem matrix.separating_left_to_linear_map₂'_iff {R₁ : Type u_2} {ι : Type u_13} [comm_ring R₁] [decidable_eq ι] [fintype ι] {M : ι R₁} :
theorem matrix.nondegenerate.to_linear_map₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] {M : ι R₁} (h : M.nondegenerate) (b : R₁ M₁) :
@[simp]
theorem matrix.separating_left_to_linear_map₂_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] {M : ι R₁} (b : R₁ M₁) :
@[simp]
theorem linear_map.nondegenerate_to_matrix₂'_iff {R₁ : Type u_2} {ι : Type u_13} [comm_ring R₁] [decidable_eq ι] [fintype ι] {B : R₁) →ₗ[R₁] R₁) →ₗ[R₁] R₁} :
theorem linear_map.separating_left.to_matrix₂' {R₁ : Type u_2} {ι : Type u_13} [comm_ring R₁] [decidable_eq ι] [fintype ι] {B : R₁) →ₗ[R₁] R₁) →ₗ[R₁] R₁} (h : B.separating_left) :
@[simp]
theorem linear_map.nondegenerate_to_matrix_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : R₁ M₁) :
theorem linear_map.separating_left.to_matrix₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (h : B.separating_left) (b : R₁ M₁) :
theorem linear_map.separating_left_to_linear_map₂'_iff_det_ne_zero {R₁ : Type u_2} {ι : Type u_13} [comm_ring R₁] [decidable_eq ι] [fintype ι] [is_domain R₁] {M : ι R₁} :
theorem linear_map.separating_left_to_linear_map₂'_of_det_ne_zero' {R₁ : Type u_2} {ι : Type u_13} [comm_ring R₁] [decidable_eq ι] [fintype ι] [is_domain R₁] (M : ι R₁) (h : M.det 0) :
theorem linear_map.separating_left_iff_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] [is_domain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : R₁ M₁) :
theorem linear_map.separating_left_of_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [comm_ring R₁] [add_comm_monoid M₁] [module R₁ M₁] [decidable_eq ι] [fintype ι] [is_domain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : R₁ M₁) (h : ( B).det 0) :