Bilinear form #
This file defines the conversion between bilinear forms and matrices.
Main definitions #
matrix.to_bilingiven a basis define a bilinear formmatrix.to_bilin'define the bilinear form onn → Rbilin_form.to_matrix: calculate the matrix coefficients of a bilinear formbilin_form.to_matrix': calculate the matrix coefficients of a bilinear form onn → R
Notations #
In this file we use the following type variables:
M,M', ... are modules over the semiringR,M₁,M₁', ... are modules over the ringR₁,M₂,M₂', ... are modules over the commutative semiringR₂,M₃,M₃', ... are modules over the commutative ringR₃,V, ... is a vector space over the fieldK.
Tags #
bilinear_form, matrix, basis
def
matrix.to_bilin'_aux
{R₂ : Type u_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
(M : matrix n n R₂) :
bilin_form R₂ (n → R₂)
The map from matrix n n R to bilinear forms on n → R.
This is an auxiliary definition for the equivalence matrix.to_bilin_form'.
Equations
- M.to_bilin'_aux = {bilin := λ (v w : n → R₂), ∑ (i j : n), ((v i) * M i j) * w j, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
theorem
matrix.to_bilin'_aux_std_basis
{R₂ : Type u_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₂)
(i j : n) :
⇑(M.to_bilin'_aux) (⇑(linear_map.std_basis R₂ (λ (_x : n), R₂) i) 1) (⇑(linear_map.std_basis R₂ (λ (_x : n), R₂) j) 1) = M i j
def
bilin_form.to_matrix_aux
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{n : Type u_11}
(b : n → M₂) :
bilin_form R₂ M₂ →ₗ[R₂] matrix n n R₂
The linear map from bilinear forms to matrix n n R given an n-indexed basis.
This is an auxiliary definition for the equivalence matrix.to_bilin_form'.
Equations
- bilin_form.to_matrix_aux b = {to_fun := λ (B : bilin_form R₂ M₂) (i j : n), ⇑B (b i) (b j), map_add' := _, map_smul' := _}
theorem
to_bilin'_aux_to_matrix_aux
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B₃ : bilin_form R₃ (n → R₃)) :
(⇑(bilin_form.to_matrix_aux (λ (j : n), ⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)) B₃).to_bilin'_aux = B₃
to_matrix' section #
This section deals with the conversion between matrices and bilinear forms on n → R₃.
def
bilin_form.to_matrix'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
bilin_form R₃ (n → R₃) ≃ₗ[R₃] matrix n n R₃
The linear equivalence between bilinear forms on n → R and n × n matrices
Equations
- bilin_form.to_matrix' = {to_fun := (bilin_form.to_matrix_aux (λ (j : n), ⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)).to_fun, map_add' := _, map_smul' := _, inv_fun := matrix.to_bilin'_aux _inst_16, left_inv := _, right_inv := _}
@[simp]
theorem
bilin_form.to_matrix_aux_std_basis
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃)) :
⇑(bilin_form.to_matrix_aux (λ (j : n), ⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)) B = ⇑bilin_form.to_matrix' B
def
matrix.to_bilin'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
matrix n n R₃ ≃ₗ[R₃] bilin_form R₃ (n → R₃)
The linear equivalence between n × n matrices and bilinear forms on n → R
Equations
@[simp]
theorem
matrix.to_bilin'_aux_eq
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₃) :
theorem
matrix.to_bilin'_apply
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₃)
(x y : n → R₃) :
theorem
matrix.to_bilin'_apply'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₃)
(v w : n → R₃) :
@[simp]
theorem
matrix.to_bilin'_std_basis
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₃)
(i j : n) :
⇑(⇑matrix.to_bilin' M) (⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) i) 1) (⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1) = M i j
@[simp]
theorem
bilin_form.to_matrix'_symm
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_bilin'_symm
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_bilin'_to_matrix'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃)) :
@[simp]
theorem
bilin_form.to_matrix'_to_bilin'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₃) :
@[simp]
theorem
bilin_form.to_matrix'_apply
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃))
(i j : n) :
⇑bilin_form.to_matrix' B i j = ⇑B (⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) i) 1) (⇑(linear_map.std_basis R₃ (λ (_x : n), R₃) j) 1)
@[simp]
theorem
bilin_form.to_matrix'_comp
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
[decidable_eq o]
(B : bilin_form R₃ (n → R₃))
(l r : (o → R₃) →ₗ[R₃] n → R₃) :
theorem
bilin_form.to_matrix'_comp_left
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃))
(f : (n → R₃) →ₗ[R₃] n → R₃) :
theorem
bilin_form.to_matrix'_comp_right
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃))
(f : (n → R₃) →ₗ[R₃] n → R₃) :
theorem
bilin_form.mul_to_matrix'_mul
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
[decidable_eq o]
(B : bilin_form R₃ (n → R₃))
(M : matrix o n R₃)
(N : matrix n o R₃) :
M ⬝ ⇑bilin_form.to_matrix' B ⬝ N = ⇑bilin_form.to_matrix' (B.comp (⇑matrix.to_lin' Mᵀ) (⇑matrix.to_lin' N))
theorem
bilin_form.mul_to_matrix'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃))
(M : matrix n n R₃) :
theorem
bilin_form.to_matrix'_mul
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₃ (n → R₃))
(M : matrix n n R₃) :
theorem
matrix.to_bilin'_comp
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
[decidable_eq o]
(M : matrix n n R₃)
(P Q : matrix n o R₃) :
(⇑matrix.to_bilin' M).comp (⇑matrix.to_lin' P) (⇑matrix.to_lin' Q) = ⇑matrix.to_bilin' (Pᵀ ⬝ M ⬝ Q)
to_matrix section #
This section deals with the conversion between matrices and bilinear forms on a module with a fixed basis.
noncomputable
def
bilin_form.to_matrix
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃) :
bilin_form R₃ M₃ ≃ₗ[R₃] matrix n n 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
noncomputable
def
matrix.to_bilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃) :
matrix n n R₃ ≃ₗ[R₃] bilin_form R₃ M₃
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
basis.equiv_fun_symm_std_basis
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(i : n) :
@[simp]
theorem
bilin_form.to_matrix_apply
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃)
(i j : n) :
@[simp]
theorem
matrix.to_bilin_apply
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(M : matrix n n R₃)
(x y : M₃) :
theorem
bilinear_form.to_matrix_aux_eq
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃) :
⇑(bilin_form.to_matrix_aux ⇑b) B = ⇑(bilin_form.to_matrix b) B
@[simp]
theorem
bilin_form.to_matrix_symm
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃) :
@[simp]
theorem
matrix.to_bilin_symm
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃) :
theorem
matrix.to_bilin_basis_fun
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
theorem
bilin_form.to_matrix_basis_fun
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_bilin_to_matrix
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃) :
⇑(matrix.to_bilin b) (⇑(bilin_form.to_matrix b) B) = B
@[simp]
theorem
bilin_form.to_matrix_to_bilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(M : matrix n n R₃) :
⇑(bilin_form.to_matrix b) (⇑(matrix.to_bilin b) M) = M
theorem
bilin_form.to_matrix_comp
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
(b : basis n R₃ M₃)
{M₃' : Type u_13}
[add_comm_group M₃']
[module R₃ M₃']
(c : basis o R₃ M₃')
[decidable_eq o]
(B : bilin_form R₃ M₃)
(l r : M₃' →ₗ[R₃] M₃) :
⇑(bilin_form.to_matrix c) (B.comp l r) = (⇑(linear_map.to_matrix c b) l)ᵀ ⬝ ⇑(bilin_form.to_matrix b) B ⬝ ⇑(linear_map.to_matrix c b) r
theorem
bilin_form.to_matrix_comp_left
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃)
(f : M₃ →ₗ[R₃] M₃) :
⇑(bilin_form.to_matrix b) (B.comp_left f) = (⇑(linear_map.to_matrix b b) f)ᵀ ⬝ ⇑(bilin_form.to_matrix b) B
theorem
bilin_form.to_matrix_comp_right
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃)
(f : M₃ →ₗ[R₃] M₃) :
⇑(bilin_form.to_matrix b) (B.comp_right f) = ⇑(bilin_form.to_matrix b) B ⬝ ⇑(linear_map.to_matrix b b) f
@[simp]
theorem
bilin_form.to_matrix_mul_basis_to_matrix
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
(b : basis n R₃ M₃)
[decidable_eq o]
(c : basis o R₃ M₃)
(B : bilin_form R₃ M₃) :
theorem
bilin_form.mul_to_matrix_mul
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
(b : basis n R₃ M₃)
{M₃' : Type u_13}
[add_comm_group M₃']
[module R₃ M₃']
(c : basis o R₃ M₃')
[decidable_eq o]
(B : bilin_form R₃ M₃)
(M : matrix o n R₃)
(N : matrix n o R₃) :
M ⬝ ⇑(bilin_form.to_matrix b) B ⬝ N = ⇑(bilin_form.to_matrix c) (B.comp (⇑(matrix.to_lin c b) Mᵀ) (⇑(matrix.to_lin c b) N))
theorem
bilin_form.mul_to_matrix
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃)
(M : matrix n n R₃) :
M ⬝ ⇑(bilin_form.to_matrix b) B = ⇑(bilin_form.to_matrix b) (B.comp_left (⇑(matrix.to_lin b b) Mᵀ))
theorem
bilin_form.to_matrix_mul
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(b : basis n R₃ M₃)
(B : bilin_form R₃ M₃)
(M : matrix n n R₃) :
⇑(bilin_form.to_matrix b) B ⬝ M = ⇑(bilin_form.to_matrix b) (B.comp_right (⇑(matrix.to_lin b b) M))
theorem
matrix.to_bilin_comp
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
{o : Type u_12}
[fintype n]
[fintype o]
[decidable_eq n]
(b : basis n R₃ M₃)
{M₃' : Type u_13}
[add_comm_group M₃']
[module R₃ M₃']
(c : basis o R₃ M₃')
[decidable_eq o]
(M : matrix n n R₃)
(P Q : matrix n o R₃) :
(⇑(matrix.to_bilin b) M).comp (⇑(matrix.to_lin c b) P) (⇑(matrix.to_lin c b) Q) = ⇑(matrix.to_bilin c) (Pᵀ ⬝ M ⬝ Q)
def
matrix.is_self_adjoint
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J A : matrix n n R₃) :
Prop
The condition for a square matrix A to be self-adjoint with respect to the square matrix
J.
Equations
- J.is_self_adjoint A = J.is_adjoint_pair J A A
def
matrix.is_skew_adjoint
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J A : matrix n n R₃) :
Prop
The condition for a square matrix A to be skew-adjoint with respect to the square matrix
J.
Equations
- J.is_skew_adjoint A = J.is_adjoint_pair J A (-A)
@[simp]
theorem
is_adjoint_pair_to_bilin'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J J₃ A A' : matrix n n R₃)
[decidable_eq n] :
(⇑matrix.to_bilin' J).is_adjoint_pair (⇑matrix.to_bilin' J₃) (⇑matrix.to_lin' A) (⇑matrix.to_lin' A') ↔ J.is_adjoint_pair J₃ A A'
@[simp]
theorem
is_adjoint_pair_to_bilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{n : Type u_11}
[fintype n]
(b : basis n R₃ M₃)
(J J₃ A A' : matrix n n R₃)
[decidable_eq n] :
(⇑(matrix.to_bilin b) J).is_adjoint_pair (⇑(matrix.to_bilin b) J₃) (⇑(matrix.to_lin b b) A) (⇑(matrix.to_lin b b) A') ↔ J.is_adjoint_pair J₃ A A'
def
pair_self_adjoint_matrices_submodule
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J J₃ : matrix n n R₃)
[decidable_eq n] :
The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
given matrices J, J₂.
@[simp]
theorem
mem_pair_self_adjoint_matrices_submodule
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J J₃ A : matrix n n R₃)
[decidable_eq n] :
A ∈ pair_self_adjoint_matrices_submodule J J₃ ↔ J.is_adjoint_pair J₃ A A
def
self_adjoint_matrices_submodule
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J : matrix n n R₃)
[decidable_eq n] :
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_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J A : matrix n n R₃)
[decidable_eq n] :
def
skew_adjoint_matrices_submodule
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J : matrix n n R₃)
[decidable_eq n] :
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_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J A : matrix n n R₃)
[decidable_eq n] :
theorem
matrix.nondegenerate_to_bilin'_iff_nondegenerate_to_bilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₃}
(b : basis ι R₃ M₃) :
(⇑matrix.to_bilin' M).nondegenerate ↔ (⇑(matrix.to_bilin b) M).nondegenerate
theorem
matrix.nondegenerate.to_bilin'
{R₃ : Type u_7}
[comm_ring R₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₃}
(h : M.nondegenerate) :
@[simp]
theorem
matrix.nondegenerate_to_bilin'_iff
{R₃ : Type u_7}
[comm_ring R₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₃} :
theorem
matrix.nondegenerate.to_bilin
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₃}
(h : M.nondegenerate)
(b : basis ι R₃ M₃) :
(⇑(matrix.to_bilin b) M).nondegenerate
@[simp]
theorem
matrix.nondegenerate_to_bilin_iff
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι R₃}
(b : basis ι R₃ M₃) :
(⇑(matrix.to_bilin b) M).nondegenerate ↔ M.nondegenerate
@[simp]
theorem
bilin_form.nondegenerate_to_matrix'_iff
{R₃ : Type u_7}
[comm_ring R₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{B : bilin_form R₃ (ι → R₃)} :
theorem
bilin_form.nondegenerate.to_matrix'
{R₃ : Type u_7}
[comm_ring R₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{B : bilin_form R₃ (ι → R₃)}
(h : B.nondegenerate) :
@[simp]
theorem
bilin_form.nondegenerate_to_matrix_iff
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{B : bilin_form R₃ M₃}
(b : basis ι R₃ M₃) :
(⇑(bilin_form.to_matrix b) B).nondegenerate ↔ B.nondegenerate
theorem
bilin_form.nondegenerate.to_matrix
{R₃ : Type u_7}
{M₃ : Type u_8}
[comm_ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{B : bilin_form R₃ M₃}
(h : B.nondegenerate)
(b : basis ι R₃ M₃) :
(⇑(bilin_form.to_matrix b) B).nondegenerate
theorem
bilin_form.nondegenerate_to_bilin'_iff_det_ne_zero
{A : Type u_11}
[comm_ring A]
[is_domain A]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{M : matrix ι ι A} :
(⇑matrix.to_bilin' M).nondegenerate ↔ M.det ≠ 0
theorem
bilin_form.nondegenerate_to_bilin'_of_det_ne_zero'
{A : Type u_11}
[comm_ring A]
[is_domain A]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
(M : matrix ι ι A)
(h : M.det ≠ 0) :
theorem
bilin_form.nondegenerate_iff_det_ne_zero
{M₃ : Type u_8}
[add_comm_group M₃]
{A : Type u_11}
[comm_ring A]
[is_domain A]
[module A M₃]
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
{B : bilin_form A M₃}
(b : basis ι A M₃) :
B.nondegenerate ↔ (⇑(bilin_form.to_matrix b) B).det ≠ 0
theorem
bilin_form.nondegenerate_of_det_ne_zero
{M₃ : Type u_8}
[add_comm_group M₃]
{A : Type u_11}
[comm_ring A]
[is_domain A]
[module A M₃]
(B₃ : bilin_form A M₃)
{ι : Type u_12}
[decidable_eq ι]
[fintype ι]
(b : basis ι A M₃)
(h : (⇑(bilin_form.to_matrix b) B₃).det ≠ 0) :