Documentation

Mathlib.LinearAlgebra.Matrix.BilinearForm

Bilinear form #

This file defines the conversion between bilinear forms and matrices.

Main definitions #

Notations #

In this file we use the following type variables:

Tags #

bilinear form, bilin form, BilinearForm, matrix, basis

def Matrix.toBilin'Aux {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] (M : Matrix n n R₂) :
LinearMap.BilinForm R₂ (nR₂)

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

This is an auxiliary definition for the equivalence Matrix.toBilin'.

Equations
Instances For
    theorem Matrix.toBilin'Aux_stdBasis {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (M : Matrix n n R₂) (i : n) (j : n) :
    (M.toBilin'Aux ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) = M i j
    def BilinForm.toMatrixAux {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} (b : nM₂) :
    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
    Instances For
      @[simp]
      theorem LinearMap.BilinForm.toMatrixAux_apply {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} (B : LinearMap.BilinForm R₂ M₂) (b : nM₂) (i : n) (j : n) :
      (BilinForm.toMatrixAux b) B i j = (B (b i)) (b j)
      theorem toBilin'Aux_toMatrixAux {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B₂ : LinearMap.BilinForm R₂ (nR₂)) :
      ((BilinForm.toMatrixAux fun (j : n) => (LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) B₂).toBilin'Aux = B₂

      ToMatrix' section #

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

      def LinearMap.BilinForm.toMatrix' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :
      LinearMap.BilinForm R₂ (nR₂) ≃ₗ[R₂] Matrix n n R₂

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

      Equations
      Instances For
        @[simp]
        theorem LinearMap.BilinForm.toMatrixAux_stdBasis {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) :
        (BilinForm.toMatrixAux fun (j : n) => (LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1) B = LinearMap.BilinForm.toMatrix' B
        def Matrix.toBilin' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :
        Matrix n n R₂ ≃ₗ[R₂] LinearMap.BilinForm R₂ (nR₂)

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

        Equations
        • Matrix.toBilin' = LinearMap.BilinForm.toMatrix'.symm
        Instances For
          @[simp]
          theorem Matrix.toBilin'Aux_eq {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (M : Matrix n n R₂) :
          M.toBilin'Aux = Matrix.toBilin' M
          theorem Matrix.toBilin'_apply {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (M : Matrix n n R₂) (x : nR₂) (y : nR₂) :
          ((Matrix.toBilin' M) x) y = i : n, j : n, x i * M i j * y j
          theorem Matrix.toBilin'_apply' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (M : Matrix n n R₂) (v : nR₂) (w : nR₂) :
          ((Matrix.toBilin' M) v) w = Matrix.dotProduct v (M.mulVec w)
          @[simp]
          theorem Matrix.toBilin'_stdBasis {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [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
          @[simp]
          theorem LinearMap.BilinForm.toMatrix'_symm {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :
          LinearMap.BilinForm.toMatrix'.symm = Matrix.toBilin'
          @[simp]
          theorem Matrix.toBilin'_symm {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :
          Matrix.toBilin'.symm = LinearMap.BilinForm.toMatrix'
          @[simp]
          theorem Matrix.toBilin'_toMatrix' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) :
          Matrix.toBilin' (LinearMap.BilinForm.toMatrix' B) = B
          @[simp]
          theorem LinearMap.BilinForm.toMatrix'_toBilin' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (M : Matrix n n R₂) :
          LinearMap.BilinForm.toMatrix' (Matrix.toBilin' M) = M
          @[simp]
          theorem LinearMap.BilinForm.toMatrix'_apply {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) (i : n) (j : n) :
          LinearMap.BilinForm.toMatrix' B i j = (B ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : n) => R₂) j) 1)
          @[simp]
          theorem LinearMap.BilinForm.toMatrix'_comp {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} {o : Type u_12} [Fintype n] [Fintype o] [DecidableEq n] [DecidableEq o] (B : LinearMap.BilinForm R₂ (nR₂)) (l : (oR₂) →ₗ[R₂] nR₂) (r : (oR₂) →ₗ[R₂] nR₂) :
          LinearMap.BilinForm.toMatrix' (B.comp l r) = (LinearMap.toMatrix' l).transpose * LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' r
          theorem LinearMap.BilinForm.toMatrix'_compLeft {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) (f : (nR₂) →ₗ[R₂] nR₂) :
          LinearMap.BilinForm.toMatrix' (B.compLeft f) = (LinearMap.toMatrix' f).transpose * LinearMap.BilinForm.toMatrix' B
          theorem LinearMap.BilinForm.toMatrix'_compRight {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) (f : (nR₂) →ₗ[R₂] nR₂) :
          LinearMap.BilinForm.toMatrix' (B.compRight f) = LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' f
          theorem LinearMap.BilinForm.mul_toMatrix'_mul {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} {o : Type u_12} [Fintype n] [Fintype o] [DecidableEq n] [DecidableEq o] (B : LinearMap.BilinForm R₂ (nR₂)) (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))
          theorem LinearMap.BilinForm.mul_toMatrix' {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) (M : Matrix n n R₂) :
          M * LinearMap.BilinForm.toMatrix' B = LinearMap.BilinForm.toMatrix' (B.compLeft (Matrix.toLin' M.transpose))
          theorem LinearMap.BilinForm.toMatrix'_mul {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] (B : LinearMap.BilinForm R₂ (nR₂)) (M : Matrix n n R₂) :
          LinearMap.BilinForm.toMatrix' B * M = LinearMap.BilinForm.toMatrix' (B.compRight (Matrix.toLin' M))
          theorem Matrix.toBilin'_comp {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} {o : Type u_12} [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.

          noncomputable def BilinForm.toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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
          Instances For
            noncomputable def Matrix.toBilin {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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
            Instances For
              @[simp]
              theorem BilinForm.toMatrix_apply {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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)
              @[simp]
              theorem Matrix.toBilin_apply {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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
              theorem BilinearForm.toMatrixAux_eq {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [Fintype n] [DecidableEq n] (b : Basis n R₂ M₂) (B : LinearMap.BilinForm R₂ M₂) :
              @[simp]
              theorem BilinForm.toMatrix_symm {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [Fintype n] [DecidableEq n] (b : Basis n R₂ M₂) :
              @[simp]
              theorem Matrix.toBilin_symm {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [Fintype n] [DecidableEq n] (b : Basis n R₂ M₂) :
              theorem Matrix.toBilin_basisFun {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :
              Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.toBilin'
              theorem BilinForm.toMatrix_basisFun {R₂ : Type u_5} [CommSemiring R₂] {n : Type u_11} [Fintype n] [DecidableEq n] :
              BilinForm.toMatrix (Pi.basisFun R₂ n) = LinearMap.BilinForm.toMatrix'
              @[simp]
              theorem Matrix.toBilin_toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [Fintype n] [DecidableEq n] (b : Basis n R₂ M₂) (B : LinearMap.BilinForm R₂ M₂) :
              @[simp]
              theorem BilinForm.toMatrix_toBilin {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [Fintype n] [DecidableEq n] (b : Basis n R₂ M₂) (M : Matrix n n R₂) :
              theorem BilinForm.toMatrix_comp {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₂ M₂) {M₂' : Type u_13} [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
              theorem BilinForm.toMatrix_compLeft {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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
              theorem BilinForm.toMatrix_compRight {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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
              @[simp]
              theorem BilinForm.toMatrix_mul_basis_toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [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
              theorem BilinForm.mul_toMatrix_mul {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₂ M₂) {M₂' : Type u_13} [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))
              theorem BilinForm.mul_toMatrix {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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))
              theorem BilinForm.toMatrix_mul {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} [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))
              theorem Matrix.toBilin_comp {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {n : Type u_11} {o : Type u_12} [Fintype n] [Fintype o] [DecidableEq n] (b : Basis n R₂ M₂) {M₂' : Type u_13} [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)
              @[simp]
              theorem isAdjointPair_toBilin' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [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'
              @[simp]
              theorem isAdjointPair_toBilin {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] {n : Type u_11} [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'
              theorem Matrix.isAdjointPair_equiv' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [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⁻¹)
              def pairSelfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [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
              Instances For
                theorem mem_pairSelfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [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
                def selfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [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
                Instances For
                  theorem mem_selfAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [Fintype n] (J : Matrix n n R₃) (A : Matrix n n R₃) [DecidableEq n] :
                  A selfAdjointMatricesSubmodule J J.IsSelfAdjoint A
                  def skewAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [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
                  Instances For
                    theorem mem_skewAdjointMatricesSubmodule' {R₃ : Type u_7} [CommRing R₃] {n : Type u_11} [Fintype n] (J : Matrix n n R₃) (A : Matrix n n R₃) [DecidableEq n] :
                    A skewAdjointMatricesSubmodule J J.IsSkewAdjoint A
                    theorem Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin {R₂ : Type u_5} {M₂ : Type u_6} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₂} (b : Basis ι R₂ M₂) :
                    (Matrix.toBilin' M).Nondegenerate ((Matrix.toBilin b) M).Nondegenerate
                    theorem Matrix.Nondegenerate.toBilin' {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₃} (h : M.Nondegenerate) :
                    (Matrix.toBilin' M).Nondegenerate
                    @[simp]
                    theorem Matrix.nondegenerate_toBilin'_iff {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₃} :
                    (Matrix.toBilin' M).Nondegenerate M.Nondegenerate
                    theorem Matrix.Nondegenerate.toBilin {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₃} (h : M.Nondegenerate) (b : Basis ι R₃ M₃) :
                    ((Matrix.toBilin b) M).Nondegenerate
                    @[simp]
                    theorem Matrix.nondegenerate_toBilin_iff {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] {ι : Type u_12} [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

                    @[simp]
                    theorem LinearMap.BilinForm.nondegenerate_toMatrix'_iff {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₃ (ιR₃)} :
                    (LinearMap.BilinForm.toMatrix' B).Nondegenerate B.Nondegenerate
                    theorem LinearMap.BilinForm.Nondegenerate.toMatrix' {R₃ : Type u_7} [CommRing R₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₃ (ιR₃)} (h : B.Nondegenerate) :
                    (LinearMap.BilinForm.toMatrix' B).Nondegenerate
                    @[simp]
                    theorem LinearMap.BilinForm.nondegenerate_toMatrix_iff {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm R₃ M₃} (b : Basis ι R₃ M₃) :
                    ((BilinForm.toMatrix b) B).Nondegenerate B.Nondegenerate
                    theorem LinearMap.BilinForm.Nondegenerate.toMatrix {R₃ : Type u_7} {M₃ : Type u_8} [CommRing R₃] [AddCommGroup M₃] [Module R₃ M₃] {ι : Type u_12} [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

                    theorem LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero {A : Type u_11} [CommRing A] [IsDomain A] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {M : Matrix ι ι A} :
                    (Matrix.toBilin' M).Nondegenerate M.det 0
                    theorem LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero' {A : Type u_11} [CommRing A] [IsDomain A] {ι : Type u_12} [DecidableEq ι] [Fintype ι] (M : Matrix ι ι A) (h : M.det 0) :
                    (Matrix.toBilin' M).Nondegenerate
                    theorem LinearMap.BilinForm.nondegenerate_iff_det_ne_zero {M₃ : Type u_8} [AddCommGroup M₃] {A : Type u_11} [CommRing A] [IsDomain A] [Module A M₃] {ι : Type u_12} [DecidableEq ι] [Fintype ι] {B : LinearMap.BilinForm A M₃} (b : Basis ι A M₃) :
                    B.Nondegenerate ((BilinForm.toMatrix b) B).det 0
                    theorem LinearMap.BilinForm.nondegenerate_of_det_ne_zero {M₃ : Type u_8} [AddCommGroup M₃] {A : Type u_11} [CommRing A] [IsDomain A] [Module A M₃] (B₃ : LinearMap.BilinForm A M₃) {ι : Type u_12} [DecidableEq ι] [Fintype ι] (b : Basis ι A M₃) (h : ((BilinForm.toMatrix b) B₃).det 0) :
                    B₃.Nondegenerate