[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
⊢ AddHom.toFun src✝.toAddHom ⁅T, S⁆ = ⁅AddHom.toFun src✝.toAddHom T, AddHom.toFun src✝.toAddHom S⁆
[PROOFSTEP]
let f := @LinearMap.toMatrix' R _ n n _ _
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ AddHom.toFun src✝.toAddHom ⁅T, S⁆ = ⁅AddHom.toFun src✝.toAddHom T, AddHom.toFun src✝.toAddHom S⁆
[PROOFSTEP]
change f (T.comp S - S.comp T) = f T * f S - f S * f T
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ ↑f (LinearMap.comp T S - LinearMap.comp S T) = ↑f T * ↑f S - ↑f S * ↑f T
[PROOFSTEP]
have h : ∀ T S : Module.End R _, f (T.comp S) = f T * f S := LinearMap.toMatrix'_comp
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
src✝ : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h : ∀ (T S : Module.End R (n → R)), ↑f (LinearMap.comp T S) = ↑f T * ↑f S
⊢ ↑f (LinearMap.comp T S - LinearMap.comp S T) = ↑f T * ↑f S - ↑f S * ↑f T
[PROOFSTEP]
rw [LinearEquiv.map_sub, h, h]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ ↑(lieConj P h) A = P * A * P⁻¹
[PROOFSTEP]
simp [LinearEquiv.conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp, LinearMap.toMatrix'_toLin']
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ ↑(LieEquiv.symm (lieConj P h)) A = P⁻¹ * A * P
[PROOFSTEP]
simp [LinearEquiv.symm_conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp, LinearMap.toMatrix'_toLin']
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type w₁
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
src✝ : Matrix n n R ≃ₗ[R] Matrix m m R := reindexLinearEquiv R R e e
x✝¹ x✝ : Matrix n n R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(reindex e e),
              map_add' :=
                (_ :
                  ∀ (x y : Matrix n n R),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : Matrix n n R),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ⁅x✝¹, x✝⁆ =
    ⁅AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(reindex e e),
                map_add' :=
                  (_ :
                    ∀ (x y : Matrix n n R),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : Matrix n n R),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x✝¹,
      AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(reindex e e),
                map_add' :=
                  (_ :
                    ∀ (x y : Matrix n n R),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : Matrix n n R),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x✝⁆
[PROOFSTEP]
simp only [LieRing.of_associative_ring_bracket, Matrix.reindex_apply, Matrix.submatrix_mul_equiv, Matrix.submatrix_sub,
  Pi.sub_apply]
