Documentation

Mathlib.LinearAlgebra.Matrix.ToLin

Linear maps and matrices #

This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.

Main definitions #

In the list below, and in all this file, R is a commutative ring (semiring is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite types used for indexing.

Issues #

This file was originally written without attention to non-commutative rings, and so mostly only works in the commutative setting. This should be fixed.

In particular, Matrix.mulVec gives us a linear equivalence Matrix m n R ≃ₗ[R] (n → R) →ₗ[Rᵐᵒᵖ] (m → R) while Matrix.vecMul gives us a linear equivalence Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] (n → R). At present, the first equivalence is developed in detail but only for commutative rings (and we omit the distinction between Rᵐᵒᵖ and R), while the second equivalence is developed only in brief, but for not-necessarily-commutative rings.

Naming is slightly inconsistent between the two developments. In the original (commutative) development linear is abbreviated to lin, although this is not consistent with the rest of mathlib. In the new (non-commutative) development linear is not abbreviated, and declarations use _right to indicate they use the right action of matrices on vectors (via Matrix.vecMul). When the two developments are made uniform, the names should be made uniform, too, by choosing between linear and lin consistently, and (presumably) adding _left where necessary.

Tags #

linear_map, matrix, linear_equiv, diagonal, det, trace

def Matrix.vecMulLinear {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) :
(mR) →ₗ[R] nR

Matrix.vecMul M is a linear map.

Equations
  • M.vecMulLinear = { toFun := fun (x : mR) => Matrix.vecMul x M, map_add' := , map_smul' := }
Instances For
    @[simp]
    theorem Matrix.vecMulLinear_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) (x : mR) :
    M.vecMulLinear x = Matrix.vecMul x M
    theorem Matrix.coe_vecMulLinear {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) :
    M.vecMulLinear = fun (v : mR) => Matrix.vecMul v M
    @[simp, deprecated Matrix.single_one_vecMul]
    theorem Matrix.vecMul_stdBasis {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] (M : Matrix m n R) (i : m) (j : n) :
    Matrix.vecMul ((LinearMap.stdBasis R (fun (x : m) => R) i) 1) M j = M i j
    theorem range_vecMulLinear {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) :
    theorem Matrix.vecMul_injective_iff {m : Type u_3} {n : Type u_4} [Fintype m] {R : Type u_5} [CommRing R] {M : Matrix m n R} :
    (Function.Injective fun (v : mR) => Matrix.vecMul v M) LinearIndependent R fun (i : m) => M i
    def LinearMap.toMatrixRight' {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] :
    ((mR) →ₗ[R] nR) ≃ₗ[Rᵐᵒᵖ] Matrix m n R

    Linear maps (m → R) →ₗ[R] (n → R) are linearly equivalent over Rᵐᵒᵖ to Matrix m n R, by having matrices act by right multiplication.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]
      abbrev Matrix.toLinearMapRight' {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] :
      Matrix m n R ≃ₗ[Rᵐᵒᵖ] (mR) →ₗ[R] nR

      A Matrix m n R is linearly equivalent over Rᵐᵒᵖ to a linear map (m → R) →ₗ[R] (n → R), by having matrices act by right multiplication.

      Equations
      • Matrix.toLinearMapRight' = LinearMap.toMatrixRight'.symm
      Instances For
        @[simp]
        theorem Matrix.toLinearMapRight'_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] (M : Matrix m n R) (v : mR) :
        (Matrix.toLinearMapRight' M) v = Matrix.vecMul v M
        @[simp]
        theorem Matrix.toLinearMapRight'_mul {R : Type u_1} [Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) :
        Matrix.toLinearMapRight' (M * N) = Matrix.toLinearMapRight' N ∘ₗ Matrix.toLinearMapRight' M
        theorem Matrix.toLinearMapRight'_mul_apply {R : Type u_1} [Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) (x : lR) :
        (Matrix.toLinearMapRight' (M * N)) x = (Matrix.toLinearMapRight' N) ((Matrix.toLinearMapRight' M) x)
        @[simp]
        theorem Matrix.toLinearMapRight'_one {R : Type u_1} [Semiring R] {m : Type u_3} [Fintype m] [DecidableEq m] :
        Matrix.toLinearMapRight' 1 = LinearMap.id
        @[simp]
        theorem Matrix.toLinearEquivRight'OfInv_symm_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : mR) :
        ∀ (a_1 : n), (Matrix.toLinearEquivRight'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLinearMapRight' M) a a_1
        @[simp]
        theorem Matrix.toLinearEquivRight'OfInv_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : nR) :
        ∀ (a_1 : m), (Matrix.toLinearEquivRight'OfInv hMM' hM'M) a a_1 = (Matrix.toLinearMapRight' M') a a_1
        def Matrix.toLinearEquivRight'OfInv {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) :
        (nR) ≃ₗ[R] mR

        If M and M' are each other's inverse matrices, they provide an equivalence between n → A and m → A corresponding to M.vecMul and M'.vecMul.

        Equations
        • Matrix.toLinearEquivRight'OfInv hMM' hM'M = { toFun := (Matrix.toLinearMapRight' M'), map_add' := , map_smul' := , invFun := (Matrix.toLinearMapRight' M), left_inv := , right_inv := }
        Instances For

          From this point on, we only work with commutative rings, and fail to distinguish between Rᵐᵒᵖ and R. This should eventually be remedied.

          def Matrix.mulVecLin {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) :
          (nR) →ₗ[R] mR

          Matrix.mulVec M is a linear map.

          Equations
          • M.mulVecLin = { toFun := M.mulVec, map_add' := , map_smul' := }
          Instances For
            theorem Matrix.coe_mulVecLin {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) :
            M.mulVecLin = M.mulVec
            @[simp]
            theorem Matrix.mulVecLin_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) (v : nR) :
            M.mulVecLin v = M.mulVec v
            @[simp]
            theorem Matrix.mulVecLin_zero {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] :
            @[simp]
            theorem Matrix.mulVecLin_add {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) (N : Matrix m n R) :
            (M + N).mulVecLin = M.mulVecLin + N.mulVecLin
            @[simp]
            theorem Matrix.mulVecLin_transpose {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype m] (M : Matrix m n R) :
            M.transpose.mulVecLin = M.vecMulLinear
            @[simp]
            theorem Matrix.vecMulLinear_transpose {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) :
            M.transpose.vecMulLinear = M.mulVecLin
            theorem Matrix.mulVecLin_submatrix {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype n] [Fintype l] (f₁ : mk) (e₂ : n l) (M : Matrix k l R) :
            (M.submatrix f₁ e₂).mulVecLin = LinearMap.funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ LinearMap.funLeft R R e₂.symm
            theorem Matrix.mulVecLin_reindex {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype n] [Fintype l] (e₁ : k m) (e₂ : l n) (M : Matrix k l R) :
            ((Matrix.reindex e₁ e₂) M).mulVecLin = (LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ (LinearEquiv.funCongrLeft R R e₂)

            A variant of Matrix.mulVecLin_submatrix that keeps around LinearEquivs.

            @[simp]
            theorem Matrix.mulVecLin_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [Fintype n] [DecidableEq n] :
            Matrix.mulVecLin 1 = LinearMap.id
            @[simp]
            theorem Matrix.mulVecLin_mul {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype n] [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
            (M * N).mulVecLin = M.mulVecLin ∘ₗ N.mulVecLin
            theorem Matrix.ker_mulVecLin_eq_bot_iff {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] {M : Matrix m n R} :
            LinearMap.ker M.mulVecLin = ∀ (v : nR), M.mulVec v = 0v = 0
            @[deprecated Matrix.mulVec_single_one]
            theorem Matrix.mulVec_stdBasis {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix m n R) (i : m) (j : n) :
            M.mulVec ((LinearMap.stdBasis R (fun (x : n) => R) j) 1) i = M i j
            @[simp, deprecated Matrix.mulVec_single_one]
            theorem Matrix.mulVec_stdBasis_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix m n R) (j : n) :
            M.mulVec ((LinearMap.stdBasis R (fun (x : n) => R) j) 1) = M.transpose j
            theorem Matrix.range_mulVecLin {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) :
            LinearMap.range M.mulVecLin = Submodule.span R (Set.range M.transpose)
            theorem Matrix.mulVec_injective_iff {m : Type u_4} {n : Type u_5} [Fintype n] {R : Type u_6} [CommRing R] {M : Matrix m n R} :
            Function.Injective M.mulVec LinearIndependent R fun (i : n) => M.transpose i
            def LinearMap.toMatrix' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] :
            ((nR) →ₗ[R] mR) ≃ₗ[R] Matrix m n R

            Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to Matrix m n R.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Matrix.toLin' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] :
              Matrix m n R ≃ₗ[R] (nR) →ₗ[R] mR

              A Matrix m n R is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R).

              Note that the forward-direction does not require DecidableEq and is Matrix.vecMulLin.

              Equations
              • Matrix.toLin' = LinearMap.toMatrix'.symm
              Instances For
                theorem Matrix.toLin'_apply' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) :
                Matrix.toLin' M = M.mulVecLin
                @[simp]
                theorem LinearMap.toMatrix'_symm {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] :
                LinearMap.toMatrix'.symm = Matrix.toLin'
                @[simp]
                theorem Matrix.toLin'_symm {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] :
                Matrix.toLin'.symm = LinearMap.toMatrix'
                @[simp]
                theorem LinearMap.toMatrix'_toLin' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) :
                LinearMap.toMatrix' (Matrix.toLin' M) = M
                @[simp]
                theorem Matrix.toLin'_toMatrix' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (f : (nR) →ₗ[R] mR) :
                Matrix.toLin' (LinearMap.toMatrix' f) = f
                @[simp]
                theorem LinearMap.toMatrix'_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (f : (nR) →ₗ[R] mR) (i : m) (j : n) :
                LinearMap.toMatrix' f i j = f (fun (j' : n) => if j' = j then 1 else 0) i
                @[simp]
                theorem Matrix.toLin'_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) (v : nR) :
                (Matrix.toLin' M) v = M.mulVec v
                @[simp]
                theorem Matrix.toLin'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                Matrix.toLin' 1 = LinearMap.id
                @[simp]
                theorem LinearMap.toMatrix'_id {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                LinearMap.toMatrix' LinearMap.id = 1
                @[simp]
                theorem LinearMap.toMatrix'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                LinearMap.toMatrix' 1 = 1
                @[simp]
                theorem Matrix.toLin'_mul {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) :
                Matrix.toLin' (M * N) = Matrix.toLin' M ∘ₗ Matrix.toLin' N
                @[simp]
                theorem Matrix.toLin'_submatrix {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype l] [DecidableEq l] (f₁ : mk) (e₂ : n l) (M : Matrix k l R) :
                Matrix.toLin' (M.submatrix f₁ e₂) = LinearMap.funLeft R R f₁ ∘ₗ Matrix.toLin' M ∘ₗ LinearMap.funLeft R R e₂.symm
                theorem Matrix.toLin'_reindex {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype l] [DecidableEq l] (e₁ : k m) (e₂ : l n) (M : Matrix k l R) :
                Matrix.toLin' ((Matrix.reindex e₁ e₂) M) = (LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ Matrix.toLin' M ∘ₗ (LinearEquiv.funCongrLeft R R e₂)

                A variant of Matrix.toLin'_submatrix that keeps around LinearEquivs.

                theorem Matrix.toLin'_mul_apply {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) (x : nR) :
                (Matrix.toLin' (M * N)) x = (Matrix.toLin' M) ((Matrix.toLin' N) x)

                Shortcut lemma for Matrix.toLin'_mul and LinearMap.comp_apply

                theorem LinearMap.toMatrix'_comp {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype l] [DecidableEq l] (f : (nR) →ₗ[R] mR) (g : (lR) →ₗ[R] nR) :
                LinearMap.toMatrix' (f ∘ₗ g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
                theorem LinearMap.toMatrix'_mul {R : Type u_1} [CommSemiring R] {m : Type u_4} [Fintype m] [DecidableEq m] (f : (mR) →ₗ[R] mR) (g : (mR) →ₗ[R] mR) :
                LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
                @[simp]
                theorem LinearMap.toMatrix'_algebraMap {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (x : R) :
                LinearMap.toMatrix' ((algebraMap R (Module.End R (nR))) x) = (Matrix.scalar n) x
                theorem Matrix.ker_toLin'_eq_bot_iff {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] {M : Matrix n n R} :
                LinearMap.ker (Matrix.toLin' M) = ∀ (v : nR), M.mulVec v = 0v = 0
                theorem Matrix.range_toLin' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) :
                LinearMap.range (Matrix.toLin' M) = Submodule.span R (Set.range M.transpose)
                @[simp]
                theorem Matrix.toLin'OfInv_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : mR) :
                ∀ (a_1 : n), (Matrix.toLin'OfInv hMM' hM'M) a a_1 = (Matrix.toLin' M') a a_1
                @[simp]
                theorem Matrix.toLin'OfInv_symm_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : nR) :
                ∀ (a_1 : m), (Matrix.toLin'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLin' M) a a_1
                def Matrix.toLin'OfInv {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) :
                (mR) ≃ₗ[R] nR

                If M and M' are each other's inverse matrices, they provide an equivalence between m → A and n → A corresponding to M.mulVec and M'.mulVec.

                Equations
                • Matrix.toLin'OfInv hMM' hM'M = { toFun := (Matrix.toLin' M'), map_add' := , map_smul' := , invFun := (Matrix.toLin' M), left_inv := , right_inv := }
                Instances For
                  def LinearMap.toMatrixAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                  ((nR) →ₗ[R] nR) ≃ₐ[R] Matrix n n R

                  Linear maps (n → R) →ₗ[R] (n → R) are algebra equivalent to Matrix n n R.

                  Equations
                  Instances For
                    def Matrix.toLinAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                    Matrix n n R ≃ₐ[R] (nR) →ₗ[R] nR

                    A Matrix n n R is algebra equivalent to a linear map (n → R) →ₗ[R] (n → R).

                    Equations
                    • Matrix.toLinAlgEquiv' = LinearMap.toMatrixAlgEquiv'.symm
                    Instances For
                      @[simp]
                      theorem LinearMap.toMatrixAlgEquiv'_symm {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                      LinearMap.toMatrixAlgEquiv'.symm = Matrix.toLinAlgEquiv'
                      @[simp]
                      theorem Matrix.toLinAlgEquiv'_symm {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                      Matrix.toLinAlgEquiv'.symm = LinearMap.toMatrixAlgEquiv'
                      @[simp]
                      theorem LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
                      LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M
                      @[simp]
                      theorem Matrix.toLinAlgEquiv'_toMatrixAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (nR) →ₗ[R] nR) :
                      Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f
                      @[simp]
                      theorem LinearMap.toMatrixAlgEquiv'_apply {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (nR) →ₗ[R] nR) (i : n) (j : n) :
                      LinearMap.toMatrixAlgEquiv' f i j = f (fun (j' : n) => if j' = j then 1 else 0) i
                      @[simp]
                      theorem Matrix.toLinAlgEquiv'_apply {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix n n R) (v : nR) :
                      (Matrix.toLinAlgEquiv' M) v = M.mulVec v
                      theorem Matrix.toLinAlgEquiv'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                      Matrix.toLinAlgEquiv' 1 = LinearMap.id
                      @[simp]
                      theorem LinearMap.toMatrixAlgEquiv'_id {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
                      LinearMap.toMatrixAlgEquiv' LinearMap.id = 1
                      theorem LinearMap.toMatrixAlgEquiv'_comp {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (nR) →ₗ[R] nR) (g : (nR) →ₗ[R] nR) :
                      LinearMap.toMatrixAlgEquiv' (f ∘ₗ g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g
                      theorem LinearMap.toMatrixAlgEquiv'_mul {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (nR) →ₗ[R] nR) (g : (nR) →ₗ[R] nR) :
                      LinearMap.toMatrixAlgEquiv' (f * g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g
                      def LinearMap.toMatrix {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) :
                      (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R

                      Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.

                      Equations
                      • LinearMap.toMatrix v₁ v₂ = (v₁.equivFun.arrowCongr v₂.equivFun).trans LinearMap.toMatrix'
                      Instances For
                        theorem LinearMap.toMatrix_eq_toMatrix' {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] :
                        LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix'

                        LinearMap.toMatrix' is a particular case of LinearMap.toMatrix, for the standard basis Pi.basisFun R n.

                        def Matrix.toLin {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) :
                        Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂

                        Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between matrices over R indexed by the bases and linear maps M₁ →ₗ M₂.

                        Equations
                        Instances For
                          theorem Matrix.toLin_eq_toLin' {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] :
                          Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'

                          Matrix.toLin' is a particular case of Matrix.toLin, for the standard basis Pi.basisFun R n.

                          @[simp]
                          theorem LinearMap.toMatrix_symm {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) :
                          (LinearMap.toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂
                          @[simp]
                          theorem Matrix.toLin_symm {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) :
                          (Matrix.toLin v₁ v₂).symm = LinearMap.toMatrix v₁ v₂
                          @[simp]
                          theorem Matrix.toLin_toMatrix {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) :
                          (Matrix.toLin v₁ v₂) ((LinearMap.toMatrix v₁ v₂) f) = f
                          @[simp]
                          theorem LinearMap.toMatrix_toLin {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (M : Matrix m n R) :
                          (LinearMap.toMatrix v₁ v₂) ((Matrix.toLin v₁ v₂) M) = M
                          theorem LinearMap.toMatrix_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
                          (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
                          theorem LinearMap.toMatrix_transpose_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) :
                          ((LinearMap.toMatrix v₁ v₂) f).transpose j = (v₂.repr (f (v₁ j)))
                          theorem LinearMap.toMatrix_apply' {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
                          (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
                          theorem LinearMap.toMatrix_transpose_apply' {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) :
                          ((LinearMap.toMatrix v₁ v₂) f).transpose j = (v₂.repr (f (v₁ j)))
                          theorem LinearMap.toMatrix_id {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                          (LinearMap.toMatrix v₁ v₁) LinearMap.id = 1

                          This will be a special case of LinearMap.toMatrix_id_eq_basis_toMatrix.

                          @[simp]
                          theorem LinearMap.toMatrix_one {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                          (LinearMap.toMatrix v₁ v₁) 1 = 1
                          @[simp]
                          theorem Matrix.toLin_one {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                          (Matrix.toLin v₁ v₁) 1 = LinearMap.id
                          theorem LinearMap.toMatrix_reindexRange {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
                          (LinearMap.toMatrix v₁.reindexRange v₂.reindexRange) f v₂ k, v₁ i, = (LinearMap.toMatrix v₁ v₂) f k i
                          @[simp]
                          theorem LinearMap.toMatrix_algebraMap {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (x : R) :
                          (LinearMap.toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (Matrix.scalar n) x
                          theorem LinearMap.toMatrix_mulVec_repr {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (x : M₁) :
                          ((LinearMap.toMatrix v₁ v₂) f).mulVec (v₁.repr x) = (v₂.repr (f x))
                          @[simp]
                          theorem LinearMap.toMatrix_basis_equiv {R : Type u_1} [CommSemiring R] {l : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype l] [DecidableEq l] (b : Basis l R M₁) (b' : Basis l R M₂) :
                          (LinearMap.toMatrix b' b) (b'.equiv b (Equiv.refl l)) = 1
                          theorem LinearMap.toMatrix_smulBasis_left {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {G : Type u_7} [Group G] [DistribMulAction G M₁] [SMulCommClass G R M₁] (g : G) (f : M₁ →ₗ[R] M₂) :
                          (LinearMap.toMatrix (g v₁) v₂) f = (LinearMap.toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g)
                          theorem LinearMap.toMatrix_smulBasis_right {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {G : Type u_7} [Group G] [DistribMulAction G M₂] [SMulCommClass G R M₂] (g : G) (f : M₁ →ₗ[R] M₂) :
                          (LinearMap.toMatrix v₁ (g v₂)) f = (LinearMap.toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f)
                          theorem Matrix.toLin_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (M : Matrix m n R) (v : M₁) :
                          ((Matrix.toLin v₁ v₂) M) v = j : m, M.mulVec (⇑(v₁.repr v)) j v₂ j
                          @[simp]
                          theorem Matrix.toLin_self {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (M : Matrix m n R) (i : n) :
                          ((Matrix.toLin v₁ v₂) M) (v₁ i) = j : m, M j i v₂ j
                          theorem LinearMap.toMatrix_comp {R : Type u_1} [CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
                          (LinearMap.toMatrix v₁ v₃) (f ∘ₗ g) = (LinearMap.toMatrix v₂ v₃) f * (LinearMap.toMatrix v₁ v₂) g
                          theorem LinearMap.toMatrix_mul {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₁) :
                          (LinearMap.toMatrix v₁ v₁) (f * g) = (LinearMap.toMatrix v₁ v₁) f * (LinearMap.toMatrix v₁ v₁) g
                          theorem LinearMap.toMatrix_pow {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (k : ) :
                          (LinearMap.toMatrix v₁ v₁) f ^ k = (LinearMap.toMatrix v₁ v₁) (f ^ k)
                          theorem Matrix.toLin_mul {R : Type u_1} [CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) :
                          (Matrix.toLin v₁ v₃) (A * B) = (Matrix.toLin v₂ v₃) A ∘ₗ (Matrix.toLin v₁ v₂) B
                          theorem Matrix.toLin_mul_apply {R : Type u_1} [CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) (x : M₁) :
                          ((Matrix.toLin v₁ v₃) (A * B)) x = ((Matrix.toLin v₂ v₃) A) (((Matrix.toLin v₁ v₂) B) x)

                          Shortcut lemma for Matrix.toLin_mul and LinearMap.comp_apply.

                          @[simp]
                          theorem Matrix.toLinOfInv_symm_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : M₂) :
                          (Matrix.toLinOfInv v₁ v₂ hMM' hM'M).symm a = ((Matrix.toLin v₂ v₁) M') a
                          @[simp]
                          theorem Matrix.toLinOfInv_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : M₁) :
                          (Matrix.toLinOfInv v₁ v₂ hMM' hM'M) a = ((Matrix.toLin v₁ v₂) M) a
                          def Matrix.toLinOfInv {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) :
                          M₁ ≃ₗ[R] M₂

                          If M and M are each other's inverse matrices, Matrix.toLin M and Matrix.toLin M' form a linear equivalence.

                          Equations
                          Instances For
                            def LinearMap.toMatrixAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                            (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R

                            Given a basis of a module M₁ over a commutative ring R, we get an algebra equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis.

                            Equations
                            Instances For
                              def Matrix.toLinAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                              Matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁

                              Given a basis of a module M₁ over a commutative ring R, we get an algebra equivalence between square matrices over R indexed by the basis and linear maps M₁ →ₗ M₁.

                              Equations
                              Instances For
                                @[simp]
                                theorem LinearMap.toMatrixAlgEquiv_symm {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                                @[simp]
                                theorem Matrix.toLinAlgEquiv_symm {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                                @[simp]
                                theorem Matrix.toLinAlgEquiv_toMatrixAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) :
                                @[simp]
                                theorem LinearMap.toMatrixAlgEquiv_toLinAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (M : Matrix n n R) :
                                theorem LinearMap.toMatrixAlgEquiv_apply {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i : n) (j : n) :
                                (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
                                theorem LinearMap.toMatrixAlgEquiv_transpose_apply {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) :
                                ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = (v₁.repr (f (v₁ j)))
                                theorem LinearMap.toMatrixAlgEquiv_apply' {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i : n) (j : n) :
                                (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
                                theorem LinearMap.toMatrixAlgEquiv_transpose_apply' {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) :
                                ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = (v₁.repr (f (v₁ j)))
                                theorem Matrix.toLinAlgEquiv_apply {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (M : Matrix n n R) (v : M₁) :
                                ((Matrix.toLinAlgEquiv v₁) M) v = j : n, M.mulVec (⇑(v₁.repr v)) j v₁ j
                                @[simp]
                                theorem Matrix.toLinAlgEquiv_self {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (M : Matrix n n R) (i : n) :
                                ((Matrix.toLinAlgEquiv v₁) M) (v₁ i) = j : n, M j i v₁ j
                                theorem LinearMap.toMatrixAlgEquiv_id {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                                (LinearMap.toMatrixAlgEquiv v₁) LinearMap.id = 1
                                theorem Matrix.toLinAlgEquiv_one {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) :
                                (Matrix.toLinAlgEquiv v₁) 1 = LinearMap.id
                                theorem LinearMap.toMatrixAlgEquiv_reindexRange {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k : n) (i : n) :
                                (LinearMap.toMatrixAlgEquiv v₁.reindexRange) f v₁ k, v₁ i, = (LinearMap.toMatrixAlgEquiv v₁) f k i
                                theorem LinearMap.toMatrixAlgEquiv_comp {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₁) :
                                theorem LinearMap.toMatrixAlgEquiv_mul {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₁) :
                                theorem Matrix.toLinAlgEquiv_mul {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (A : Matrix n n R) (B : Matrix n n R) :
                                (Matrix.toLinAlgEquiv v₁) (A * B) = (Matrix.toLinAlgEquiv v₁) A ∘ₗ (Matrix.toLinAlgEquiv v₁) B
                                @[simp]
                                theorem Matrix.toLin_finTwoProd_apply {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) (d : R) (x : R × R) :
                                ((Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d]) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)
                                theorem Matrix.toLin_finTwoProd {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) (d : R) :
                                (Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d] = (a LinearMap.fst R R R + b LinearMap.snd R R R).prod (c LinearMap.fst R R R + d LinearMap.snd R R R)
                                @[simp]
                                theorem toMatrix_distrib_mul_action_toLinearMap {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (x : R) :
                                (LinearMap.toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun (x_1 : n) => x
                                theorem LinearMap.toMatrix_prodMap {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] [DecidableEq (n m)] (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) :
                                (LinearMap.toMatrix (v₁.prod v₂) (v₁.prod v₂)) (LinearMap.prodMap φ₁ φ₂) = Matrix.fromBlocks ((LinearMap.toMatrix v₁ v₁) φ₁) 0 0 ((LinearMap.toMatrix v₂ v₂) φ₂)
                                theorem Algebra.toMatrix_lmul' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) (i : m) (j : m) :
                                (LinearMap.toMatrix b b) ((Algebra.lmul R S) x) i j = (b.repr (x * b j)) i
                                @[simp]
                                theorem Algebra.toMatrix_lsmul {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : R) :
                                (LinearMap.toMatrix b b) ((Algebra.lsmul R R S) x) = Matrix.diagonal fun (x_1 : m) => x
                                noncomputable def Algebra.leftMulMatrix {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) :
                                S →ₐ[R] Matrix m m R

                                leftMulMatrix b x is the matrix corresponding to the linear map fun y ↦ x * y.

                                leftMulMatrix_eq_repr_mul gives a formula for the entries of leftMulMatrix.

                                This definition is useful for doing (more) explicit computations with LinearMap.mulLeft, such as the trace form or norm map for algebras.

                                Equations
                                Instances For
                                  theorem Algebra.leftMulMatrix_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) :
                                  theorem Algebra.leftMulMatrix_eq_repr_mul {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) (i : m) (j : m) :
                                  (Algebra.leftMulMatrix b) x i j = (b.repr (x * b j)) i
                                  theorem Algebra.leftMulMatrix_mulVec_repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) (y : S) :
                                  ((Algebra.leftMulMatrix b) x).mulVec (b.repr y) = (b.repr (x * y))
                                  @[simp]
                                  theorem Algebra.toMatrix_lmul_eq {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) :
                                  theorem Algebra.leftMulMatrix_injective {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) :
                                  @[simp]
                                  theorem Algebra.smul_leftMulMatrix {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) {G : Type u_4} [Group G] [DistribMulAction G S] [SMulCommClass G R S] [SMulCommClass G S S] (g : G) (x : S) :
                                  theorem Algebra.smulTower_leftMulMatrix {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : T) (ik : m × n) (jk : m × n) :
                                  (Algebra.leftMulMatrix (b.smulTower c)) x ik jk = (Algebra.leftMulMatrix b) ((Algebra.leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1
                                  theorem Algebra.smulTower_leftMulMatrix_algebraMap {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : S) :
                                  (Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) = Matrix.blockDiagonal fun (x_1 : n) => (Algebra.leftMulMatrix b) x
                                  theorem Algebra.smulTower_leftMulMatrix_algebraMap_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : S) (i : m) (j : m) (k : n) :
                                  (Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (Algebra.leftMulMatrix b) x i j
                                  theorem Algebra.smulTower_leftMulMatrix_algebraMap_ne {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : S) (i : m) (j : m) {k : n} {k' : n} (h : k k') :
                                  (Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0
                                  def algEquivMatrix' {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] :
                                  Module.End R (nR) ≃ₐ[R] Matrix n n R

                                  The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the algebra structures.

                                  Equations
                                  • algEquivMatrix' = { toFun := (↑LinearMap.toMatrix').toFun, invFun := LinearMap.toMatrix'.invFun, left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := }
                                  Instances For
                                    def LinearEquiv.algConj {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :

                                    A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.

                                    Equations
                                    • e.algConj = { toFun := (↑e.conj).toFun, invFun := e.conj.invFun, left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := }
                                    Instances For
                                      def algEquivMatrix {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] {M : Type u_3} [AddCommGroup M] [Module R M] [Fintype n] (h : Basis n R M) :

                                      A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.

                                      Equations
                                      Instances For
                                        theorem Basis.linearMap_repr_symm_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) :
                                        ∀ (a : ι₂ × ι₁ →₀ R), (b₁.linearMap b₂).repr.symm a = (Matrix.toLin b₁ b₂) ((Finsupp.linearCombination R (Matrix.stdBasis R ι₂ ι₁)) a)
                                        @[simp]
                                        theorem Basis.linearMap_repr_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) :
                                        ∀ (a : M₁ →ₗ[R] M₂), (b₁.linearMap b₂).repr a = (Matrix.stdBasis R ι₂ ι₁).repr ((LinearMap.toMatrix b₁ b₂) a)
                                        noncomputable def Basis.linearMap {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) :
                                        Basis (ι₂ × ι₁) R (M₁ →ₗ[R] M₂)

                                        The standard basis of the space linear maps between two modules induced by a basis of the domain and codomain.

                                        If M₁ and M₂ are modules with basis b₁ and b₂ respectively indexed by finite types ι₁ and ι₂, then Basis.linearMap b₁ b₂ is the basis of M₁ →ₗ[R] M₂ indexed by ι₂ × ι₁ where (i, j) indexes the linear map that sends b j to b i and sends all other basis vectors to 0.

                                        Equations
                                        Instances For
                                          theorem Basis.linearMap_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (ij : ι₂ × ι₁) :
                                          (b₁.linearMap b₂) ij = (Matrix.toLin b₁ b₂) ((Matrix.stdBasis R ι₂ ι₁) ij)
                                          theorem Basis.linearMap_apply_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (ij : ι₂ × ι₁) (k : ι₁) :
                                          ((b₁.linearMap b₂) ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0
                                          theorem Basis.end_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) :
                                          ∀ (a : ι × ι →₀ R), b.end.repr.symm a = (Matrix.toLin b b) ((Finsupp.linearCombination R (Matrix.stdBasis R ι ι)) a)
                                          @[simp]
                                          theorem Basis.end_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) :
                                          ∀ (a : M →ₗ[R] M), b.end.repr a = (Matrix.stdBasis R ι ι).repr ((LinearMap.toMatrix b b) a)
                                          @[reducible, inline]
                                          noncomputable abbrev Basis.end {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) :
                                          Basis (ι × ι) R (Module.End R M)

                                          The standard basis of the endomorphism algebra of a module induced by a basis of the module.

                                          If M is a module with basis b indexed by a finite type ι, then Basis.end b is the basis of Module.End R M indexed by ι × ι where (i, j) indexes the linear map that sends b j to b i and sends all other basis vectors to 0.

                                          Equations
                                          • b.end = b.linearMap b
                                          Instances For
                                            theorem Basis.end_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) :
                                            b.end ij = (Matrix.toLin b b) ((Matrix.stdBasis R ι ι) ij)
                                            theorem Basis.end_apply_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) (k : ι) :
                                            (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0