Bilinear form #

This file defines the conversion between bilinear forms and matrices.

Main definitions #

Matrix.toBilin given a basis define a bilinear form
Matrix.toBilin' define the bilinear form on n → R
BilinForm.toMatrix: calculate the matrix coefficients of a bilinear form
BilinForm.toMatrix': calculate the matrix coefficients of a bilinear form on n → R

Notations #

In this file we use the following type variables:

M₁ is a module over the commutative semiring R₁,
M₂ is a module over the commutative ring R₂.

Tags #

bilinear form, bilin form, BilinearForm, matrix, basis

source

def Matrix.toBilin'Aux {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] (M : Matrix n n R₁) :

LinearMap.BilinForm 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.toBilin'.

Equations

M.toBilin'Aux = Matrix.toLinearMap₂'Aux (RingHom.id R₁) (RingHom.id R₁) M

Instances For

source

theorem Matrix.toBilin'Aux_single {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) (i : n) (j : n) :

(M.toBilin'Aux (Pi.single i 1)) (Pi.single j 1) = M i j

source

def BilinForm.toMatrixAux {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} (b : n → M₁) :

LinearMap.BilinForm 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.toBilin'.

Equations

BilinForm.toMatrixAux b = LinearMap.toMatrix₂Aux R₁ b b

Instances For

source

@[simp]

theorem LinearMap.BilinForm.toMatrixAux_apply {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} (B : LinearMap.BilinForm R₁ M₁) (b : n → M₁) (i : n) (j : n) :

(BilinForm.toMatrixAux b) B i j = (B (b i)) (b j)

source

theorem toBilin'Aux_toMatrixAux {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B₂ : LinearMap.BilinForm R₁ (n → R₁)) :

((BilinForm.toMatrixAux fun (j : n) => Pi.single j 1) B₂).toBilin'Aux = B₂

`ToMatrix'` section #

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

source

def LinearMap.BilinForm.toMatrix' {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :

LinearMap.BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁

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

Equations

LinearMap.BilinForm.toMatrix' = LinearMap.toMatrix₂' R₁

Instances For

source

def Matrix.toBilin' {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :

Matrix n n R₁ ≃ₗ[R₁] LinearMap.BilinForm R₁ (n → R₁)

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

Equations

Matrix.toBilin' = LinearMap.BilinForm.toMatrix'.symm

Instances For

source

@[simp]

theorem Matrix.toBilin'Aux_eq {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) :

M.toBilin'Aux = Matrix.toBilin' M

source

theorem Matrix.toBilin'_apply {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) (x : n → R₁) (y : n → R₁) :

((Matrix.toBilin' M) x) y = ∑ i : n, ∑ j : n, x i * M i j * y j

source

theorem Matrix.toBilin'_apply' {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) (v : n → R₁) (w : n → R₁) :

((Matrix.toBilin' M) v) w = Matrix.dotProduct v (M.mulVec w)

source

@[simp]

theorem Matrix.toBilin'_single {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) (i : n) (j : n) :

((Matrix.toBilin' M) (Pi.single i 1)) (Pi.single j 1) = M i j

source

@[simp, deprecated Matrix.toBilin'_single]

theorem Matrix.toBilin'_stdBasis {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) (i : n) (j : n) :

((Matrix.toBilin' M) ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) j) 1) = M i j

source

@[simp]

theorem LinearMap.BilinForm.toMatrix'_symm {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :

LinearMap.BilinForm.toMatrix'.symm = Matrix.toBilin'

source

@[simp]

theorem Matrix.toBilin'_symm {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :

Matrix.toBilin'.symm = LinearMap.BilinForm.toMatrix'

source

@[simp]

theorem Matrix.toBilin'_toMatrix' {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₁ (n → R₁)) :

Matrix.toBilin' (LinearMap.BilinForm.toMatrix' B) = B

source

@[simp]

theorem LinearMap.BilinForm.toMatrix'_toBilin' {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix n n R₁) :

LinearMap.BilinForm.toMatrix' (Matrix.toBilin' M) = M

source

@[simp]

theorem LinearMap.BilinForm.toMatrix'_apply {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₁ (n → R₁)) (i : n) (j : n) :

LinearMap.BilinForm.toMatrix' B i j = (B (Pi.single i 1)) (Pi.single j 1)

source

@[simp]

theorem LinearMap.BilinForm.toMatrix'_comp {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] [DecidableEq o] (B : LinearMap.BilinForm R₁ (n → R₁)) (l : (o → R₁) →ₗ[R₁] n → R₁) (r : (o → R₁) →ₗ[R₁] n → R₁) :

LinearMap.BilinForm.toMatrix' (B.comp l r) = (LinearMap.toMatrix' l).transpose * LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' r

source

theorem LinearMap.BilinForm.toMatrix'_compLeft {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₁ (n → R₁)) (f : (n → R₁) →ₗ[R₁] n → R₁) :

LinearMap.BilinForm.toMatrix' (B.compLeft f) = (LinearMap.toMatrix' f).transpose * LinearMap.BilinForm.toMatrix' B

source

theorem LinearMap.BilinForm.toMatrix'_compRight {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₁ (n → R₁)) (f : (n → R₁) →ₗ[R₁] n → R₁) :

LinearMap.BilinForm.toMatrix' (B.compRight f) = LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' f

source

theorem LinearMap.BilinForm.mul_toMatrix'_mul {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] [DecidableEq o] (B : LinearMap.BilinForm R₁ (n → R₁)) (M : Matrix o n R₁) (N : Matrix n o R₁) :

M * LinearMap.BilinForm.toMatrix' B * N = LinearMap.BilinForm.toMatrix' (B.comp (Matrix.toLin' M.transpose) (Matrix.toLin' N))

source

theorem LinearMap.BilinForm.mul_toMatrix' {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₁ (n → R₁)) (M : Matrix n n R₁) :

M * LinearMap.BilinForm.toMatrix' B = LinearMap.BilinForm.toMatrix' (B.compLeft (Matrix.toLin' M.transpose))

source

theorem LinearMap.BilinForm.toMatrix'_mul {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₁ (n → R₁)) (M : Matrix n n R₁) :

LinearMap.BilinForm.toMatrix' B * M = LinearMap.BilinForm.toMatrix' (B.compRight (Matrix.toLin' M))

source

theorem Matrix.toBilin'_comp {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] [DecidableEq o] (M : Matrix n n R₁) (P : Matrix n o R₁) (Q : Matrix n o R₁) :

(Matrix.toBilin' M).comp (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' (P.transpose * M * Q)

`ToMatrix` section #

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

source

noncomputable def BilinForm.toMatrix {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) :

LinearMap.BilinForm R₁ M₁ ≃ₗ[R₁] Matrix n n R₁

BilinForm.toMatrix 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

BilinForm.toMatrix b = LinearMap.toMatrix₂ b b

Instances For

source

noncomputable def Matrix.toBilin {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) :

Matrix n n R₁ ≃ₗ[R₁] LinearMap.BilinForm R₁ M₁

BilinForm.toMatrix 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

Matrix.toBilin b = (BilinForm.toMatrix b).symm

Instances For

source

@[simp]

theorem BilinForm.toMatrix_apply {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) (i : n) (j : n) :

(BilinForm.toMatrix b) B i j = (B (b i)) (b j)

source

@[simp]

theorem Matrix.toBilin_apply {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (M : Matrix n n R₁) (x : M₁) (y : M₁) :

(((Matrix.toBilin b) M) x) y = ∑ i : n, ∑ j : n, (b.repr x) i * M i j * (b.repr y) j

source

theorem BilinearForm.toMatrixAux_eq {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) :

(BilinForm.toMatrixAux ⇑b) B = (BilinForm.toMatrix b) B

source

@[simp]

theorem BilinForm.toMatrix_symm {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) :

(BilinForm.toMatrix b).symm = Matrix.toBilin b

source

@[simp]

theorem Matrix.toBilin_symm {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) :

(Matrix.toBilin b).symm = BilinForm.toMatrix b

source

theorem Matrix.toBilin_basisFun {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :

Matrix.toBilin (Pi.basisFun R₁ n) = Matrix.toBilin'

source

theorem BilinForm.toMatrix_basisFun {R₁ : Type u_1} [CommSemiring R₁] {n : Type u_5} [Fintype n] [DecidableEq n] :

BilinForm.toMatrix (Pi.basisFun R₁ n) = LinearMap.BilinForm.toMatrix'

source

@[simp]

theorem Matrix.toBilin_toMatrix {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) :

(Matrix.toBilin b) ((BilinForm.toMatrix b) B) = B

source

@[simp]

theorem BilinForm.toMatrix_toBilin {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (M : Matrix n n R₁) :

(BilinForm.toMatrix b) ((Matrix.toBilin b) M) = M

source

theorem BilinForm.toMatrix_comp {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₁ M₁) {M₂' : Type u_7} [AddCommMonoid M₂'] [Module R₁ M₂'] (c : Basis o R₁ M₂') [DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (l : M₂' →ₗ[R₁] M₁) (r : M₂' →ₗ[R₁] M₁) :

(BilinForm.toMatrix c) (B.comp l r) = ((LinearMap.toMatrix c b) l).transpose * (BilinForm.toMatrix b) B * (LinearMap.toMatrix c b) r

source

theorem BilinForm.toMatrix_compLeft {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁) :

(BilinForm.toMatrix b) (B.compLeft f) = ((LinearMap.toMatrix b b) f).transpose * (BilinForm.toMatrix b) B

source

theorem BilinForm.toMatrix_compRight {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) (f : M₁ →ₗ[R₁] M₁) :

(BilinForm.toMatrix b) (B.compRight f) = (BilinForm.toMatrix b) B * (LinearMap.toMatrix b b) f

source

@[simp]

theorem BilinForm.toMatrix_mul_basis_toMatrix {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₁ M₁) [DecidableEq o] (c : Basis o R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) :

(b.toMatrix ⇑c).transpose * (BilinForm.toMatrix b) B * b.toMatrix ⇑c = (BilinForm.toMatrix c) B

source

theorem BilinForm.mul_toMatrix_mul {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₁ M₁) {M₂' : Type u_7} [AddCommMonoid M₂'] [Module R₁ M₂'] (c : Basis o R₁ M₂') [DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (M : Matrix o n R₁) (N : Matrix n o R₁) :

M * (BilinForm.toMatrix b) B * N = (BilinForm.toMatrix c) (B.comp ((Matrix.toLin c b) M.transpose) ((Matrix.toLin c b) N))

source

theorem BilinForm.mul_toMatrix {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) (M : Matrix n n R₁) :

M * (BilinForm.toMatrix b) B = (BilinForm.toMatrix b) (B.compLeft ((Matrix.toLin b b) M.transpose))

source

theorem BilinForm.toMatrix_mul {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n] (b : Basis n R₁ M₁) (B : LinearMap.BilinForm R₁ M₁) (M : Matrix n n R₁) :

(BilinForm.toMatrix b) B * M = (BilinForm.toMatrix b) (B.compRight ((Matrix.toLin b b) M))

source

theorem Matrix.toBilin_comp {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {n : Type u_5} {o : Type u_6} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₁ M₁) {M₂' : Type u_7} [AddCommMonoid M₂'] [Module R₁ M₂'] (c : Basis o R₁ M₂') [DecidableEq o] (M : Matrix n n R₁) (P : Matrix n o R₁) (Q : Matrix n o R₁) :

((Matrix.toBilin b) M).comp ((Matrix.toLin c b) P) ((Matrix.toLin c b) Q) = (Matrix.toBilin c) (P.transpose * M * Q)

source

@[simp]

theorem isAdjointPair_toBilin' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) (J₃ : Matrix n n R₂) (A : Matrix n n R₂) (A' : Matrix n n R₂) [DecidableEq n] :

(Matrix.toBilin' J).IsAdjointPair (Matrix.toBilin' J₃) (Matrix.toLin' A) (Matrix.toLin' A') ↔ J.IsAdjointPair J₃ A A'

source

@[simp]

theorem isAdjointPair_toBilin {R₂ : Type u_3} {M₂ : Type u_4} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] {n : Type u_5} [Fintype n] (b : Basis n R₂ M₂) (J : Matrix n n R₂) (J₃ : Matrix n n R₂) (A : Matrix n n R₂) (A' : Matrix n n R₂) [DecidableEq n] :

((Matrix.toBilin b) J).IsAdjointPair ((Matrix.toBilin b) J₃) ((Matrix.toLin b b) A) ((Matrix.toLin b b) A') ↔ J.IsAdjointPair J₃ A A'

source

theorem Matrix.isAdjointPair_equiv' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) (A : Matrix n n R₂) (A' : Matrix n n R₂) [DecidableEq n] (P : Matrix n n R₂) (h : IsUnit P) :

(P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A A' ↔ J.IsAdjointPair J (P * A * P⁻¹) (P * A' * P⁻¹)

source

def pairSelfAdjointMatricesSubmodule' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) (J₃ : Matrix n n R₂) [DecidableEq n] :

Submodule R₂ (Matrix n n R₂)

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

Equations

pairSelfAdjointMatricesSubmodule' J J₃ = Submodule.map (↑LinearMap.toMatrix') ((Matrix.toBilin' J).isPairSelfAdjointSubmodule (Matrix.toBilin' J₃))

Instances For

source

theorem mem_pairSelfAdjointMatricesSubmodule' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) (J₃ : Matrix n n R₂) (A : Matrix n n R₂) [DecidableEq n] :

A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ J.IsAdjointPair J₃ A A

source

def selfAdjointMatricesSubmodule' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) [DecidableEq n] :

Submodule R₂ (Matrix n n R₂)

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

Equations

selfAdjointMatricesSubmodule' J = pairSelfAdjointMatricesSubmodule J J

Instances For

source

theorem mem_selfAdjointMatricesSubmodule' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) (A : Matrix n n R₂) [DecidableEq n] :

A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A

source

def skewAdjointMatricesSubmodule' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) [DecidableEq n] :

Submodule R₂ (Matrix n n R₂)

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

Equations

skewAdjointMatricesSubmodule' J = pairSelfAdjointMatricesSubmodule (-J) J

Instances For

source

theorem mem_skewAdjointMatricesSubmodule' {R₂ : Type u_3} [CommRing R₂] {n : Type u_5} [Fintype n] (J : Matrix n n R₂) (A : Matrix n n R₂) [DecidableEq n] :

A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A

source

theorem Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :

(Matrix.toBilin' M).Nondegenerate ↔ ((Matrix.toBilin b) M).Nondegenerate

source

theorem Matrix.Nondegenerate.toBilin' {R₂ : Type u_3} [CommRing R₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₂} (h : M.Nondegenerate) :

(Matrix.toBilin' M).Nondegenerate

source

@[simp]

theorem Matrix.nondegenerate_toBilin'_iff {R₂ : Type u_3} [CommRing R₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₂} :

(Matrix.toBilin' M).Nondegenerate ↔ M.Nondegenerate

source

theorem Matrix.Nondegenerate.toBilin {R₂ : Type u_3} {M₂ : Type u_4} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₂} (h : M.Nondegenerate) (b : Basis ι R₂ M₂) :

((Matrix.toBilin b) M).Nondegenerate

source

@[simp]

theorem Matrix.nondegenerate_toBilin_iff {R₂ : Type u_3} {M₂ : Type u_4} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₂} (b : Basis ι R₂ M₂) :

((Matrix.toBilin b) M).Nondegenerate ↔ M.Nondegenerate

Lemmas transferring nondegeneracy between a bilinear form and its associated matrix

source

@[simp]

theorem LinearMap.BilinForm.nondegenerate_toMatrix'_iff {R₂ : Type u_3} [CommRing R₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₂ (ι → R₂)} :

(LinearMap.BilinForm.toMatrix' B).Nondegenerate ↔ B.Nondegenerate

source

theorem LinearMap.BilinForm.Nondegenerate.toMatrix' {R₂ : Type u_3} [CommRing R₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₂ (ι → R₂)} (h : B.Nondegenerate) :

(LinearMap.BilinForm.toMatrix' B).Nondegenerate

source

@[simp]

theorem LinearMap.BilinForm.nondegenerate_toMatrix_iff {R₂ : Type u_3} {M₂ : Type u_4} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₂ M₂} (b : Basis ι R₂ M₂) :

((BilinForm.toMatrix b) B).Nondegenerate ↔ B.Nondegenerate

source

theorem LinearMap.BilinForm.Nondegenerate.toMatrix {R₂ : Type u_3} {M₂ : Type u_4} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₂ M₂} (h : B.Nondegenerate) (b : Basis ι R₂ M₂) :

((BilinForm.toMatrix b) B).Nondegenerate

Some shorthands for combining the above with Matrix.nondegenerate_of_det_ne_zero

source

theorem LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero {A : Type u_5} [CommRing A] [IsDomain A] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι A} :

(Matrix.toBilin' M).Nondegenerate ↔ M.det ≠ 0

source

theorem LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero' {A : Type u_5} [CommRing A] [IsDomain A] {ι : Type u_6} [DecidableEq ι] [Fintype ι] (M : Matrix ι ι A) (h : M.det ≠ 0) :

(Matrix.toBilin' M).Nondegenerate

source

theorem LinearMap.BilinForm.nondegenerate_iff_det_ne_zero {M₂ : Type u_4} [AddCommGroup M₂] {A : Type u_5} [CommRing A] [IsDomain A] [Module A M₂] {ι : Type u_6} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm A M₂} (b : Basis ι A M₂) :

B.Nondegenerate ↔ ((BilinForm.toMatrix b) B).det ≠ 0

source

theorem LinearMap.BilinForm.nondegenerate_of_det_ne_zero {M₂ : Type u_4} [AddCommGroup M₂] {A : Type u_5} [CommRing A] [IsDomain A] [Module A M₂] (B₃ : LinearMap.BilinForm A M₂) {ι : Type u_6} [DecidableEq ι] [Fintype ι] (b : Basis ι A M₂) (h : ((BilinForm.toMatrix b) B₃).det ≠ 0) :

B₃.Nondegenerate

HepLean Documentation

Mathlib.LinearAlgebra.Matrix.BilinearForm

Bilinear form #

Main definitions #

Notations #

Tags #

`ToMatrix'` section #

`ToMatrix` section #

Bilinear form #

Main definitions #

Notations #

Tags #

ToMatrix' section #

ToMatrix section #

`ToMatrix'` section #

`ToMatrix` section #