rw [AddMonoidHom.map_trace]
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    (Ideal.Quotient.mk p).toAddMonoidHom ((leftMulMatrix b) x).trace
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotientOfLocalRing b)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x)).trace =
    ((Ideal.Quotient.mk p).toAddMonoidHom.mapMatrix ((leftMulMatrix b) x)).trace