Documentation

Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Sesquilinear form #

This file defines the conversion between sesquilinear maps and matrices.

Main definitions #

TODO #

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

Tags #

Sesquilinear form, Sesquilinear map, matrix, basis

def Matrix.toLinearMap₂'Aux {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) (f : Matrix n m N₂) :
(nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] N₂

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

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

Equations
Instances For
    theorem Matrix.toLinearMap₂'Aux_single {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [DecidableEq n] [DecidableEq m] (f : Matrix n m N₂) (i : n) (j : m) :
    ((Matrix.toLinearMap₂'Aux σ₁ σ₂ f) (Pi.single i 1)) (Pi.single j 1) = f i j
    def LinearMap.toMatrix₂Aux (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid N₂] [Module R N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} (b₁ : nM₁) (b₂ : mM₂) :
    (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂

    The linear map from sesquilinear maps to Matrix n m N₂ 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
    Instances For
      @[simp]
      theorem LinearMap.toMatrix₂Aux_apply (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid N₂] [Module R N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) (b₁ : nM₁) (b₂ : mM₂) (i : n) (j : m) :
      (LinearMap.toMatrix₂Aux R b₁ b₂) f i j = (f (b₁ i)) (b₂ j)
      theorem LinearMap.toLinearMap₂'Aux_toMatrix₂Aux (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid N₂] [Module R N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (f : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] N₂) :
      Matrix.toLinearMap₂'Aux σ₁ σ₂ ((LinearMap.toMatrix₂Aux R (fun (i : n) => Pi.single i 1) fun (j : m) => Pi.single j 1) f) = f
      theorem Matrix.toMatrix₂Aux_toLinearMap₂'Aux (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [Semiring R₁] [Semiring S₁] [Semiring R₂] [Semiring S₂] [AddCommMonoid N₂] [Module R N₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (f : Matrix n m N₂) :
      (LinearMap.toMatrix₂Aux R (fun (i : n) => Pi.single i 1) fun (j : m) => Pi.single j 1) (Matrix.toLinearMap₂'Aux σ₁ σ₂ f) = f

      Bilinear maps over n → R #

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

      def LinearMap.toMatrixₛₗ₂' (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁} {σ₂ : R₂ →+* S₂} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
      ((nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] N₂) ≃ₗ[R] Matrix n m N₂

      The linear equivalence between sesquilinear maps 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) {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
        ((nS₁) →ₗ[S₁] (mS₂) →ₗ[S₂] N₂) ≃ₗ[R] Matrix n m N₂

        The linear equivalence between bilinear maps and n × m matrices

        Equations
        Instances For
          def Matrix.toLinearMapₛₗ₂' (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
          Matrix n m N₂ ≃ₗ[R] (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] N₂

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

          Equations
          Instances For
            def Matrix.toLinearMap₂' (R : Type u_1) {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
            Matrix n m N₂ ≃ₗ[R] (nS₁) →ₗ[S₁] (mS₂) →ₗ[S₂] N₂

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

            Equations
            Instances For
              theorem Matrix.toLinearMapₛₗ₂'_aux_eq {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) :
              theorem Matrix.toLinearMapₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) (x : nR₁) (y : mR₂) :
              (((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = i : n, j : m, σ₁ (x i) σ₂ (y j) M i j
              theorem Matrix.toLinearMap₂'_apply {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) (x : nS₁) (y : mS₂) :
              (((Matrix.toLinearMap₂' R) M) x) y = i : n, j : m, x i y j M i j
              theorem Matrix.toLinearMap₂'_apply' {n : Type u_12} {m : Type u_13} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] {T : Type u_17} [CommSemiring T] (M : Matrix n m T) (v : nT) (w : mT) :
              (((Matrix.toLinearMap₂' T) M) v) w = Matrix.dotProduct v (M.mulVec w)
              @[simp]
              theorem Matrix.toLinearMapₛₗ₂'_single {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) (i : n) (j : m) :
              (((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) (Pi.single i 1)) (Pi.single j 1) = M i j
              @[simp, deprecated Matrix.toLinearMapₛₗ₂'_single]
              theorem Matrix.toLinearMapₛₗ₂'_stdBasis {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) (i : n) (j : m) :
              (((Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M) ((LinearMap.stdBasis R₁ (fun (x : n) => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun (x : m) => R₂) j) 1) = M i j
              @[simp]
              theorem Matrix.toLinearMap₂'_single {R : Type u_1} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) (i : n) (j : m) :
              (((Matrix.toLinearMap₂' R) M) (Pi.single i 1)) (Pi.single j 1) = M i j
              @[simp, deprecated Matrix.toLinearMap₂'_single]
              theorem Matrix.toLinearMap₂'_stdBasis {R : Type u_1} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) (i : n) (j : m) :
              (((Matrix.toLinearMap₂' R) M) ((LinearMap.stdBasis R (fun (x : n) => R) i) 1)) ((LinearMap.stdBasis R (fun (x : m) => R) j) 1) = M i j
              @[simp]
              theorem LinearMap.toMatrixₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
              @[simp]
              theorem Matrix.toLinearMapₛₗ₂'_symm {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] :
              @[simp]
              theorem Matrix.toLinearMapₛₗ₂'_toMatrix' {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] N₂) :
              @[simp]
              theorem Matrix.toLinearMap₂'_toMatrix' {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (nS₁) →ₗ[S₁] (mS₂) →ₗ[S₂] N₂) :
              @[simp]
              theorem LinearMap.toMatrix'_toLinearMapₛₗ₂' {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) :
              @[simp]
              theorem LinearMap.toMatrix'_toLinearMap₂' {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (M : Matrix n m N₂) :
              @[simp]
              theorem LinearMap.toMatrixₛₗ₂'_apply {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring R₁] [Semiring R₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁) (σ₂ : R₂ →+* S₂) [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (nR₁) →ₛₗ[σ₁] (mR₂) →ₛₗ[σ₂] N₂) (i : n) (j : m) :
              @[simp]
              theorem LinearMap.toMatrix₂'_apply {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid N₂] [Module R N₂] [Semiring S₁] [Semiring S₂] [Module S₁ N₂] [Module S₂ N₂] [SMulCommClass S₁ R N₂] [SMulCommClass S₂ R N₂] [SMulCommClass S₂ S₁ N₂] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (B : (nS₁) →ₗ[S₁] (mS₂) →ₗ[S₂] N₂) (i : n) (j : m) :
              (LinearMap.toMatrix₂' R) B i j = (B (Pi.single i 1)) (Pi.single j 1)
              @[simp]
              theorem LinearMap.toMatrix₂'_compl₁₂ {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} {R : Type u_17} [CommSemiring 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₂' R) (B.compl₁₂ l r) = (LinearMap.toMatrix' l).transpose * (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' r
              theorem LinearMap.toMatrix₂'_comp {n : Type u_12} {m : Type u_13} {n' : Type u_14} {R : Type u_17} [CommSemiring 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₂' R) (B ∘ₗ f) = (LinearMap.toMatrix' f).transpose * (LinearMap.toMatrix₂' R) B
              theorem LinearMap.toMatrix₂'_compl₂ {n : Type u_12} {m : Type u_13} {m' : Type u_15} {R : Type u_17} [CommSemiring 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₂' R) (B.compl₂ f) = (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' f
              theorem LinearMap.mul_toMatrix₂'_mul {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} {R : Type u_17} [CommSemiring 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₂' R) B * N = (LinearMap.toMatrix₂' R) (B.compl₁₂ (Matrix.toLin' M.transpose) (Matrix.toLin' N))
              theorem LinearMap.mul_toMatrix' {n : Type u_12} {m : Type u_13} {n' : Type u_14} {R : Type u_17} [CommSemiring 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₂' R) B = (LinearMap.toMatrix₂' R) (B ∘ₗ Matrix.toLin' M.transpose)
              theorem LinearMap.toMatrix₂'_mul {n : Type u_12} {m : Type u_13} {m' : Type u_15} {R : Type u_17} [CommSemiring 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₂' R) B * M = (LinearMap.toMatrix₂' R) (B.compl₂ (Matrix.toLin' M))
              theorem Matrix.toLinearMap₂'_comp {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} {R : Type u_17} [CommSemiring 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) :
              ((Matrix.toLinearMap₂' R) M).compl₁₂ (Matrix.toLin' P) (Matrix.toLin' Q) = (Matrix.toLinearMap₂' R) (P.transpose * M * Q)

              Bilinear maps over arbitrary vector spaces #

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

              noncomputable def LinearMap.toMatrix₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
              (M₁ →ₗ[R] M₂ →ₗ[R] N₂) ≃ₗ[R] Matrix n m N₂

              LinearMap.toMatrix₂ b₁ b₂ is the equivalence between R-bilinear maps 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_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
                Matrix n m N₂ ≃ₗ[R] M₁ →ₗ[R] M₂ →ₗ[R] N₂

                Matrix.toLinearMap₂ b₁ b₂ is the equivalence between R-bilinear maps 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_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) (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_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m N₂) (x : M₁) (y : M₂) :
                  (((Matrix.toLinearMap₂ b₁ b₂) M) x) y = i : n, j : m, (b₁.repr x) i (b₂.repr y) j M i j
                  theorem LinearMap.toMatrix₂Aux_eq {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) :
                  (LinearMap.toMatrix₂Aux R b₁ b₂) B = (LinearMap.toMatrix₂ b₁ b₂) B
                  @[simp]
                  theorem LinearMap.toMatrix₂_symm {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
                  (LinearMap.toMatrix₂ b₁ b₂).symm = Matrix.toLinearMap₂ b₁ b₂
                  @[simp]
                  theorem Matrix.toLinearMap₂_symm {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) :
                  (Matrix.toLinearMap₂ b₁ b₂).symm = LinearMap.toMatrix₂ b₁ b₂
                  @[simp]
                  theorem Matrix.toLinearMap₂_toMatrix₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) :
                  (Matrix.toLinearMap₂ b₁ b₂) ((LinearMap.toMatrix₂ b₁ b₂) B) = B
                  @[simp]
                  theorem LinearMap.toMatrix₂_toLinearMap₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {N₂ : Type u_11} {n : Type u_12} {m : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] (b₁ : Basis n R M₁) (b₂ : Basis m R M₂) (M : Matrix n m N₂) :
                  (LinearMap.toMatrix₂ b₁ b₂) ((Matrix.toLinearMap₂ b₁ b₂) M) = M
                  theorem LinearMap.toMatrix₂_compl₁₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₁' : Type u_9} {M₂' : Type u_10} {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} [CommSemiring 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₂') (B.compl₁₂ l r) = ((LinearMap.toMatrix b₁' b₁) l).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * (LinearMap.toMatrix b₂' b₂) r
                  theorem LinearMap.toMatrix₂_comp {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₁' : Type u_9} {n : Type u_12} {m : Type u_13} {n' : Type u_14} [CommSemiring 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₂) (B ∘ₗ f) = ((LinearMap.toMatrix b₁' b₁) f).transpose * (LinearMap.toMatrix₂ b₁ b₂) B
                  theorem LinearMap.toMatrix₂_compl₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₂' : Type u_10} {n : Type u_12} {m : Type u_13} {m' : Type u_15} [CommSemiring 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₂') (B.compl₂ 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_7} {M₂ : Type u_8} {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} [CommSemiring 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) :
                  (b₁.toMatrix c₁).transpose * (LinearMap.toMatrix₂ b₁ b₂) B * b₂.toMatrix c₂ = (LinearMap.toMatrix₂ c₁ c₂) B
                  theorem LinearMap.mul_toMatrix₂_mul {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₁' : Type u_9} {M₂' : Type u_10} {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} [CommSemiring 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₂') (B.compl₁₂ ((Matrix.toLin b₁' b₁) M.transpose) ((Matrix.toLin b₂' b₂) N))
                  theorem LinearMap.mul_toMatrix₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₁' : Type u_9} {n : Type u_12} {m : Type u_13} {n' : Type u_14} [CommSemiring 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₂) (B ∘ₗ (Matrix.toLin b₁' b₁) M.transpose)
                  theorem LinearMap.toMatrix₂_mul {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₂' : Type u_10} {n : Type u_12} {m : Type u_13} {m' : Type u_15} [CommSemiring 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₂') (B.compl₂ ((Matrix.toLin b₂' b₂) M))
                  theorem Matrix.toLinearMap₂_compl₁₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {M₁' : Type u_9} {M₂' : Type u_10} {n : Type u_12} {m : Type u_13} {n' : Type u_14} {m' : Type u_15} [CommSemiring 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) :
                  ((Matrix.toLinearMap₂ b₁ b₂) M).compl₁₂ ((Matrix.toLin b₁' b₁) P) ((Matrix.toLin b₂' b₂) Q) = (Matrix.toLinearMap₂ b₁' b₂') (P.transpose * M * Q)

                  Adjoint pairs #

                  def Matrix.IsAdjointPair {R : Type u_1} {n : Type u_12} {n' : Type u_14} [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
                  • J.IsAdjointPair J' A A' = (A.transpose * J' = J * A')
                  Instances For
                    def Matrix.IsSelfAdjoint {R : Type u_1} {n : Type u_12} [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
                    • J.IsSelfAdjoint A₁ = J.IsAdjointPair J A₁ A₁
                    Instances For
                      def Matrix.IsSkewAdjoint {R : Type u_1} {n : Type u_12} [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
                      • J.IsSkewAdjoint A₁ = J.IsAdjointPair J A₁ (-A₁)
                      Instances For
                        @[simp]
                        theorem isAdjointPair_toLinearMap₂' {R : Type u_1} {n : Type u_12} {n' : Type u_14} [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'] :
                        ((Matrix.toLinearMap₂' R) J).IsAdjointPair ((Matrix.toLinearMap₂' R) J') (Matrix.toLin' A) (Matrix.toLin' A') J.IsAdjointPair J' A A'
                        @[simp]
                        theorem isAdjointPair_toLinearMap₂ {R : Type u_1} {M₁ : Type u_7} {M₂ : Type u_8} {n : Type u_12} {n' : Type u_14} [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'] :
                        ((Matrix.toLinearMap₂ b₁ b₁) J).IsAdjointPair ((Matrix.toLinearMap₂ b₂ b₂) J') ((Matrix.toLin b₁ b₂) A) ((Matrix.toLin b₂ b₁) A') J.IsAdjointPair J' A A'
                        theorem Matrix.isAdjointPair_equiv {R : Type u_1} {n : Type u_12} [CommRing R] [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_1} {n : Type u_12} [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_12} [CommRing R] [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_1} {n : Type u_12} [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_12} [CommRing R] [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_1} {n : Type u_12} [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_12} [CommRing R] [Fintype n] (J : Matrix n n R) (A₁ : Matrix n n R) [DecidableEq n] :
                              A₁ skewAdjointMatricesSubmodule J J.IsSkewAdjoint A₁

                              Nondegenerate bilinear forms #

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