no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix b b) f) = trace (↑(toMatrix b b) (comp (comp id f) id))
rw [LinearMap.id_comp, LinearMap.comp_id]
no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix b b) (comp (comp id f) id)) = trace (↑(toMatrix c b) id ⬝ ↑(toMatrix c c) f ⬝ ↑(toMatrix b c) id)
rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]
no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c b) id ⬝ ↑(toMatrix c c) f ⬝ ↑(toMatrix b c) id) =
    trace (↑(toMatrix c c) f ⬝ ↑(toMatrix b c) id ⬝ ↑(toMatrix c b) id)
rw [Matrix.mul_assoc, Matrix.trace_mul_comm]
no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c c) f ⬝ ↑(toMatrix b c) id ⬝ ↑(toMatrix c b) id) = trace (↑(toMatrix c c) (comp (comp f id) id))
rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]
no goals
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c c) (comp (comp f id) id)) = trace (↑(toMatrix c c) f)
rw [LinearMap.comp_id, LinearMap.comp_id]