Bilinear form #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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₂), finset.univ.sum (λ (i : n), finset.univ.sum (λ (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₂), ⇑matrix.of (λ (i j : n), ⇑B (b i) (b j)), map_add' := _, map_smul' := _}
@[simp]
theorem
bilin_form.to_matrix_aux_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{n : Type u_11}
(B : bilin_form R₂ M₂)
(b : n → M₂)
(i j : n) :
⇑(bilin_form.to_matrix_aux b) B i j = ⇑B (b i) (b j)
theorem
to_bilin'_aux_to_matrix_aux
{R₂ : Type u_5}
[comm_semiring 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_5}
[comm_semiring 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_5}
[comm_semiring 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_5}
[comm_semiring 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_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₂) :
theorem
matrix.to_bilin'_apply
{R₂ : Type u_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₂)
(x y : n → R₂) :
⇑(⇑matrix.to_bilin' M) x y = finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), x i * M i j * y j))
theorem
matrix.to_bilin'_apply'
{R₂ : Type u_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(M : matrix n n R₂)
(v w : n → R₂) :
⇑(⇑matrix.to_bilin' M) v w = matrix.dot_product v (M.mul_vec w)
@[simp]
theorem
matrix.to_bilin'_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) :
⇑(⇑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_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_bilin'_symm
{R₂ : Type u_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_bilin'_to_matrix'
{R₂ : Type u_5}
[comm_semiring 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_5}
[comm_semiring 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_5}
[comm_semiring 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_5}
[comm_semiring 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₂) :
⇑bilin_form.to_matrix' (B.comp l r) = ((⇑linear_map.to_matrix' l).transpose.mul (⇑bilin_form.to_matrix' B)).mul (⇑linear_map.to_matrix' r)
theorem
bilin_form.to_matrix'_comp_left
{R₂ : Type u_5}
[comm_semiring 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_5}
[comm_semiring 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_5}
[comm_semiring 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.mul (⇑bilin_form.to_matrix' B)).mul N = ⇑bilin_form.to_matrix' (B.comp (⇑matrix.to_lin' M.transpose) (⇑matrix.to_lin' N))
theorem
bilin_form.mul_to_matrix'
{R₂ : Type u_5}
[comm_semiring 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_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n]
(B : bilin_form R₂ (n → R₂))
(M : matrix n n R₂) :
(⇑bilin_form.to_matrix' B).mul M = ⇑bilin_form.to_matrix' (B.comp_right (⇑matrix.to_lin' M))
theorem
matrix.to_bilin'_comp
{R₂ : Type u_5}
[comm_semiring 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.transpose.mul M).mul 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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
bilin_form.to_matrix_apply
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
theorem
bilin_form.to_matrix_basis_fun
{R₂ : Type u_5}
[comm_semiring R₂]
{n : Type u_11}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_bilin_to_matrix
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_monoid 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).transpose.mul (⇑(bilin_form.to_matrix b) B)).mul (⇑(linear_map.to_matrix c b) r)
theorem
bilin_form.to_matrix_comp_left
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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).transpose.mul (⇑(bilin_form.to_matrix b) B)
theorem
bilin_form.to_matrix_comp_right
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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).mul (⇑(linear_map.to_matrix b b) f)
@[simp]
theorem
bilin_form.to_matrix_mul_basis_to_matrix
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_monoid 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.mul (⇑(bilin_form.to_matrix b) B)).mul N = ⇑(bilin_form.to_matrix c) (B.comp (⇑(matrix.to_lin c b) M.transpose) (⇑(matrix.to_lin c b) N))
theorem
bilin_form.mul_to_matrix
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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.mul (⇑(bilin_form.to_matrix b) B) = ⇑(bilin_form.to_matrix b) (B.comp_left (⇑(matrix.to_lin b b) M.transpose))
theorem
bilin_form.to_matrix_mul
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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).mul M = ⇑(bilin_form.to_matrix b) (B.comp_right (⇑(matrix.to_lin b b) M))
theorem
matrix.to_bilin_comp
{R₂ : Type u_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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_monoid 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.transpose.mul M).mul Q)
@[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'
theorem
matrix.is_adjoint_pair_equiv'
{R₃ : Type u_7}
[comm_ring R₃]
{n : Type u_11}
[fintype n]
(J A A' : matrix n n R₃)
[decidable_eq n]
(P : matrix n n R₃)
(h : is_unit P) :
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₂.
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
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
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_5}
{M₂ : Type u_6}
[comm_semiring R₂]
[add_comm_monoid 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) :