Documentation

Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Sesquilinear form #

This file defines the conversion between sesquilinear forms and matrices.

Main definitions #

Todos #

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

Tags #

sesquilinear_form, matrix, basis

def Matrix.toLinearMap₂'Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [Fintype n] [Fintype m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (f : Matrix n m R) :
(nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R

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

This is an auxiliary definition for the equivalence Matrix.toLinearMap₂'.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Matrix.toLinearMap₂'Aux_stdBasis {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [Fintype n] [Fintype m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) [DecidableEq n] [DecidableEq m] (f : Matrix n m R) (i : n) (j : m) :
    ↑(↑(Matrix.toLinearMap₂'Aux σ₁ σ₂ f) (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = f i j
    def LinearMap.toMatrix₂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} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (b₁ : nM₁) (b₂ : mM₂) :
    (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) →ₗ[R] Matrix n 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.toLinearMapₛₗ₂'.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem LinearMap.toMatrix₂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} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (b₁ : nM₁) (b₂ : mM₂) (i : n) (j : m) :
      ↑(LinearMap.toMatrix₂Aux b₁ b₂) f i j = ↑(f (b₁ i)) (b₂ j)
      theorem LinearMap.toLinearMap₂'Aux_toMatrix₂Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R) :
      Matrix.toLinearMap₂'Aux σ₁ σ₂ (↑(LinearMap.toMatrix₂Aux (fun i => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) f) = f
      theorem Matrix.toMatrix₂Aux_toLinearMap₂'Aux {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} (f : Matrix n m R) :
      ↑(LinearMap.toMatrix₂Aux (fun i => ↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1) fun j => ↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) (Matrix.toLinearMap₂'Aux σ₁ σ₂ f) = f

      Bilinear forms over n → R #

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

      def LinearMap.toMatrixₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {σ₁ : R₁ →+* R} {σ₂ : R₂ →+* R} :
      ((nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R) ≃ₗ[R] Matrix n m R

      The linear equivalence between sesquilinear forms and n × m matrices

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def LinearMap.toMatrix₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
        ((nR) →ₗ[R] (mR) →ₗ[R] R) ≃ₗ[R] Matrix n m R

        The linear equivalence between bilinear forms and n × m matrices

        Equations
        • LinearMap.toMatrix₂' = LinearMap.toMatrixₛₗ₂'
        Instances For
          def Matrix.toLinearMapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
          Matrix n m R ≃ₗ[R] (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R

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

          Equations
          Instances For
            def Matrix.toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
            Matrix n m R ≃ₗ[R] (nR) →ₗ[R] (mR) →ₗ[R] R

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

            Equations
            Instances For
              theorem Matrix.toLinearMapₛₗ₂'_aux_eq {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) :
              theorem Matrix.toLinearMapₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) (x : nR₁) (y : mR₂) :
              ↑(↑(↑(Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) x) y = Finset.sum Finset.univ fun i => Finset.sum Finset.univ fun j => σ₁ (x i) * M i j * σ₂ (y j)
              theorem Matrix.toLinearMap₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) (x : nR) (y : mR) :
              ↑(↑(Matrix.toLinearMap₂' M) x) y = Finset.sum Finset.univ fun i => Finset.sum Finset.univ fun j => x i * M i j * y j
              theorem Matrix.toLinearMap₂'_apply' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) (v : nR) (w : mR) :
              ↑(↑(Matrix.toLinearMap₂' M) v) w = Matrix.dotProduct v (Matrix.mulVec M w)
              @[simp]
              theorem Matrix.toLinearMapₛₗ₂'_stdBasis {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) (i : n) (j : m) :
              ↑(↑(↑(Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = M i j
              @[simp]
              theorem Matrix.toLinearMap₂'_stdBasis {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) (i : n) (j : m) :
              ↑(↑(Matrix.toLinearMap₂' M) (↑(LinearMap.stdBasis R (fun x => R) i) 1)) (↑(LinearMap.stdBasis R (fun x => R) j) 1) = M i j
              @[simp]
              theorem LinearMap.toMatrixₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
              LinearEquiv.symm LinearMap.toMatrixₛₗ₂' = Matrix.toLinearMapₛₗ₂' σ₁ σ₂
              @[simp]
              theorem Matrix.toLinearMapₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) :
              LinearEquiv.symm (Matrix.toLinearMapₛₗ₂' σ₁ σ₂) = LinearMap.toMatrixₛₗ₂'
              @[simp]
              theorem Matrix.toLinearMapₛₗ₂'_toMatrix' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R) :
              ↑(Matrix.toLinearMapₛₗ₂' σ₁ σ₂) (LinearMap.toMatrixₛₗ₂' B) = B
              @[simp]
              theorem Matrix.toLinearMap₂'_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) :
              Matrix.toLinearMap₂' (LinearMap.toMatrix₂' B) = B
              @[simp]
              theorem LinearMap.toMatrix'_toLinearMapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (M : Matrix n m R) :
              LinearMap.toMatrixₛₗ₂' (↑(Matrix.toLinearMapₛₗ₂' σ₁ σ₂) M) = M
              @[simp]
              theorem LinearMap.toMatrix'_toLinearMap₂' {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m R) :
              LinearMap.toMatrix₂' (Matrix.toLinearMap₂' M) = M
              @[simp]
              theorem LinearMap.toMatrixₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {n : Type u_9} {m : Type u_10} [CommRing R] [CommRing R₁] [CommRing R₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (σ₁ : R₁ →+* R) (σ₂ : R₂ →+* R) (B : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] R) (i : n) (j : m) :
              LinearMap.toMatrixₛₗ₂' B i j = ↑(B (↑(LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) (↑(LinearMap.stdBasis R₂ (fun x => R₂) j) 1)
              @[simp]
              theorem LinearMap.toMatrix₂'_apply {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (i : n) (j : m) :
              LinearMap.toMatrix₂' B i j = ↑(B (↑(LinearMap.stdBasis R (fun x => R) i) 1)) (↑(LinearMap.stdBasis R (fun x => R) j) 1)
              @[simp]
              theorem LinearMap.toMatrix₂'_compl₁₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (l : (n'R) →ₗ[R] nR) (r : (m'R) →ₗ[R] mR) :
              LinearMap.toMatrix₂' (LinearMap.compl₁₂ B l r) = Matrix.transpose (LinearMap.toMatrix' l) * LinearMap.toMatrix₂' B * LinearMap.toMatrix' r
              theorem LinearMap.toMatrix₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [DecidableEq n'] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (f : (n'R) →ₗ[R] nR) :
              LinearMap.toMatrix₂' (LinearMap.comp B f) = Matrix.transpose (LinearMap.toMatrix' f) * LinearMap.toMatrix₂' B
              theorem LinearMap.toMatrix₂'_compl₂ {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype m'] [DecidableEq m'] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (f : (m'R) →ₗ[R] mR) :
              LinearMap.toMatrix₂' (LinearMap.compl₂ B f) = LinearMap.toMatrix₂' B * LinearMap.toMatrix' f
              theorem LinearMap.mul_toMatrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :
              M * LinearMap.toMatrix₂' B * N = LinearMap.toMatrix₂' (LinearMap.compl₁₂ B (Matrix.toLin' (Matrix.transpose M)) (Matrix.toLin' N))
              theorem LinearMap.mul_toMatrix' {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [DecidableEq n'] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (M : Matrix n' n R) :
              M * LinearMap.toMatrix₂' B = LinearMap.toMatrix₂' (LinearMap.comp B (Matrix.toLin' (Matrix.transpose M)))
              theorem LinearMap.toMatrix₂'_mul {R : Type u_1} {n : Type u_9} {m : Type u_10} {m' : Type u_12} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype m'] [DecidableEq m'] (B : (nR) →ₗ[R] (mR) →ₗ[R] R) (M : Matrix m m' R) :
              LinearMap.toMatrix₂' B * M = LinearMap.toMatrix₂' (LinearMap.compl₂ B (Matrix.toLin' M))
              theorem Matrix.toLinearMap₂'_comp {R : Type u_1} {n : Type u_9} {m : Type u_10} {n' : Type u_11} {m' : Type u_12} [CommRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
              LinearMap.compl₁₂ (Matrix.toLinearMap₂' M) (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toLinearMap₂' (Matrix.transpose P * M * Q)

              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 LinearMap.toMatrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
              (M₁ →ₗ[R] M₂ →ₗ[R] R) ≃ₗ[R] Matrix n m R

              LinearMap.toMatrix₂ b₁ b₂ is the equivalence between R-bilinear forms on M and n-by-m matrices with entries in R, if b₁ and b₂ are R-bases for M₁ and M₂, respectively.

              Equations
              Instances For
                noncomputable def Matrix.toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
                Matrix n m R ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] R

                Matrix.toLinearMap₂ b₁ b₂ is the equivalence between R-bilinear forms on M and n-by-m matrices with entries in R, if b₁ and b₂ are R-bases for M₁ and M₂, respectively; this is the reverse direction of LinearMap.toMatrix₂ b₁ b₂.

                Equations
                Instances For
                  @[simp]
                  theorem LinearMap.toMatrix₂_apply {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (i : n) (j : m) :
                  ↑(LinearMap.toMatrix₂ b₁ b₂) B i j = ↑(B (b₁ i)) (b₂ j)
                  @[simp]
                  theorem Matrix.toLinearMap₂_apply {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m R) (x : M₁) (y : M₂) :
                  ↑(↑(↑(Matrix.toLinearMap₂ b₁ b₂) M) x) y = Finset.sum Finset.univ fun i => Finset.sum Finset.univ fun j => ↑(b₁.repr x) i * M i j * ↑(b₂.repr y) j
                  theorem LinearMap.toMatrix₂Aux_eq {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
                  ↑(LinearMap.toMatrix₂Aux b₁ b₂) B = ↑(LinearMap.toMatrix₂ b₁ b₂) B
                  @[simp]
                  theorem LinearMap.toMatrix₂_symm {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
                  @[simp]
                  theorem Matrix.toLinearMap₂_symm {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
                  theorem Matrix.toLinearMap₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] :
                  Matrix.toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLinearMap₂'
                  theorem LinearMap.toMatrix₂_basisFun {R : Type u_1} {n : Type u_9} {m : Type u_10} [CommRing R] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] :
                  LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂'
                  @[simp]
                  theorem Matrix.toLinearMap₂_toMatrix₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
                  ↑(Matrix.toLinearMap₂ b₁ b₂) (↑(LinearMap.toMatrix₂ b₁ b₂) B) = B
                  @[simp]
                  theorem LinearMap.toMatrix₂_toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {m : Type u_10} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m R) :
                  ↑(LinearMap.toMatrix₂ b₁ b₂) (↑(Matrix.toLinearMap₂ b₁ b₂) M) = M
                  theorem LinearMap.toMatrix₂_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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] [AddCommMonoid M₂'] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁) (r : M₂' →ₗ[R] M₂) :
                  ↑(LinearMap.toMatrix₂ b₁' b₂') (LinearMap.compl₁₂ B l r) = Matrix.transpose (↑(LinearMap.toMatrix b₁' b₁) l) * ↑(LinearMap.toMatrix₂ b₁ b₂) B * ↑(LinearMap.toMatrix b₂' b₂) r
                  theorem LinearMap.toMatrix₂_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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] (b₁' : Basis n' R M₁') [Fintype n'] [DecidableEq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₁' →ₗ[R] M₁) :
                  ↑(LinearMap.toMatrix₂ b₁' b₂) (LinearMap.comp B f) = Matrix.transpose (↑(LinearMap.toMatrix b₁' b₁) f) * ↑(LinearMap.toMatrix₂ b₁ b₂) B
                  theorem LinearMap.toMatrix₂_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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₂'] [Module R M₂'] (b₂' : Basis m' R M₂') [Fintype m'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (f : M₂' →ₗ[R] M₂) :
                  ↑(LinearMap.toMatrix₂ b₁ b₂') (LinearMap.compl₂ B f) = ↑(LinearMap.toMatrix₂ b₁ b₂) B * ↑(LinearMap.toMatrix b₂' b₂) f
                  @[simp]
                  theorem LinearMap.toMatrix₂_mul_basis_toMatrix {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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (c₁ : Basis n' R M₁) (c₂ : Basis m' R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
                  Matrix.transpose (Basis.toMatrix b₁ c₁) * ↑(LinearMap.toMatrix₂ b₁ b₂) B * Basis.toMatrix b₂ c₂ = ↑(LinearMap.toMatrix₂ c₁ c₂) B
                  theorem LinearMap.mul_toMatrix₂_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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] [AddCommMonoid M₂'] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) (N : Matrix m m' R) :
                  M * ↑(LinearMap.toMatrix₂ b₁ b₂) B * N = ↑(LinearMap.toMatrix₂ b₁' b₂') (LinearMap.compl₁₂ B (↑(Matrix.toLin b₁' b₁) (Matrix.transpose M)) (↑(Matrix.toLin b₂' b₂) N))
                  theorem LinearMap.mul_toMatrix₂ {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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] (b₁' : Basis n' R M₁') [Fintype n'] [DecidableEq n'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) :
                  M * ↑(LinearMap.toMatrix₂ b₁ b₂) B = ↑(LinearMap.toMatrix₂ b₁' b₂) (LinearMap.comp B (↑(Matrix.toLin b₁' b₁) (Matrix.transpose M)))
                  theorem LinearMap.toMatrix₂_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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₂'] [Module R M₂'] (b₂' : Basis m' R M₂') [Fintype m'] [DecidableEq m'] (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix m m' R) :
                  ↑(LinearMap.toMatrix₂ b₁ b₂) B * M = ↑(LinearMap.toMatrix₂ b₁ b₂') (LinearMap.compl₂ B (↑(Matrix.toLin b₂' b₂) M))
                  theorem Matrix.toLinearMap₂_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} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) [AddCommMonoid M₁'] [Module R M₁'] [AddCommMonoid M₂'] [Module R M₂'] (b₁' : Basis n' R M₁') (b₂' : Basis m' R M₂') [Fintype n'] [Fintype m'] [DecidableEq n'] [DecidableEq m'] (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
                  LinearMap.compl₁₂ (↑(Matrix.toLinearMap₂ b₁ b₂) M) (↑(Matrix.toLin b₁' b₁) P) (↑(Matrix.toLin b₂' b₂) Q) = ↑(Matrix.toLinearMap₂ b₁' b₂') (Matrix.transpose P * M * Q)

                  Adjoint pairs #

                  def Matrix.IsAdjointPair {R : Type u_1} {n : Type u_9} {n' : Type u_11} [CommRing R] [Fintype n] [Fintype n'] (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) :

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

                  Equations
                  Instances For
                    def Matrix.IsSelfAdjoint {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) :

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

                    Equations
                    Instances For
                      def Matrix.IsSkewAdjoint {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) :

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

                      Equations
                      Instances For
                        @[simp]
                        theorem isAdjointPair_toLinearMap₂' {R : Type u_1} {n : Type u_9} {n' : Type u_11} [CommRing R] [Fintype n] [Fintype n'] (J : Matrix n n R) (J' : Matrix n' n' R) (A : Matrix n' n R) (A' : Matrix n n' R) [DecidableEq n] [DecidableEq n'] :
                        LinearMap.IsAdjointPair (Matrix.toLinearMap₂' J) (Matrix.toLinearMap₂' J') (Matrix.toLin' A) (Matrix.toLin' A') Matrix.IsAdjointPair J J' A A'
                        @[simp]
                        theorem isAdjointPair_toLinearMap₂ {R : Type u_1} {M₁ : Type u_5} {M₂ : Type u_6} {n : Type u_9} {n' : Type u_11} [CommRing R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Fintype n] [Fintype n'] (b₁ : Basis n R M₁) (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] [DecidableEq n'] :
                        LinearMap.IsAdjointPair (↑(Matrix.toLinearMap₂ b₁ b₁) J) (↑(Matrix.toLinearMap₂ b₂ b₂) J') (↑(Matrix.toLin b₁ b₂) A) (↑(Matrix.toLin b₂ b₁) A') Matrix.IsAdjointPair J J' A A'
                        theorem Matrix.isAdjointPair_equiv {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] (P : Matrix n n R) (h : IsUnit P) :
                        Matrix.IsAdjointPair (Matrix.transpose P * J * P) (Matrix.transpose P * J * P) A₁ A₁ Matrix.IsAdjointPair J J (P * A₁ * P⁻¹) (P * A₁ * P⁻¹)
                        def pairSelfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [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
                          @[simp]
                          theorem mem_pairSelfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (J₂ : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :
                          def selfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [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
                            @[simp]
                            theorem mem_selfAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :
                            def skewAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [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
                              @[simp]
                              theorem mem_skewAdjointMatricesSubmodule {R : Type u_1} {n : Type u_9} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :

                              Nondegenerate bilinear forms #

                              theorem Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
                              theorem Matrix.Nondegenerate.toLinearMap₂' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (h : Matrix.Nondegenerate M) :
                              LinearMap.SeparatingLeft (Matrix.toLinearMap₂' M)
                              @[simp]
                              theorem Matrix.separatingLeft_toLinearMap₂'_iff {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} :
                              LinearMap.SeparatingLeft (Matrix.toLinearMap₂' M) Matrix.Nondegenerate M
                              theorem Matrix.Nondegenerate.toLinearMap₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (h : Matrix.Nondegenerate M) (b : Basis ι R₁ M₁) :
                              @[simp]
                              theorem Matrix.separatingLeft_toLinearMap₂_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {M : Matrix ι ι R₁} (b : Basis ι R₁ M₁) :
                              @[simp]
                              theorem LinearMap.nondegenerate_toMatrix₂'_iff {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {B : (ιR₁) →ₗ[R₁] (ιR₁) →ₗ[R₁] R₁} :
                              Matrix.Nondegenerate (LinearMap.toMatrix₂' B) LinearMap.SeparatingLeft B
                              theorem LinearMap.SeparatingLeft.toMatrix₂' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] {B : (ιR₁) →ₗ[R₁] (ιR₁) →ₗ[R₁] R₁} (h : LinearMap.SeparatingLeft B) :
                              Matrix.Nondegenerate (LinearMap.toMatrix₂' B)
                              @[simp]
                              theorem LinearMap.nondegenerate_toMatrix_iff {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :
                              theorem LinearMap.SeparatingLeft.toMatrix₂ {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (h : LinearMap.SeparatingLeft B) (b : Basis ι R₁ M₁) :
                              theorem LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] [IsDomain R₁] {M : Matrix ι ι R₁} :
                              LinearMap.SeparatingLeft (Matrix.toLinearMap₂' M) Matrix.det M 0
                              theorem LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero' {R₁ : Type u_2} {ι : Type u_13} [CommRing R₁] [DecidableEq ι] [Fintype ι] [IsDomain R₁] (M : Matrix ι ι R₁) (h : Matrix.det M 0) :
                              LinearMap.SeparatingLeft (Matrix.toLinearMap₂' M)
                              theorem LinearMap.separatingLeft_iff_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] [IsDomain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) :
                              theorem LinearMap.separatingLeft_of_det_ne_zero {R₁ : Type u_2} {M₁ : Type u_5} {ι : Type u_13} [CommRing R₁] [AddCommMonoid M₁] [Module R₁ M₁] [DecidableEq ι] [Fintype ι] [IsDomain R₁] {B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁} (b : Basis ι R₁ M₁) (h : Matrix.det (↑(LinearMap.toMatrix₂ b b) B) 0) :