no goals
ι : Type ?u.28957
m : Type u_2
n : Type u_3
p : Type u_4
α : Type ?u.28969
R : Type u_1
S : Type ?u.28975
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ trace (A ⬝ B ⬝ C) = trace (C ⬝ A ⬝ B)
rw [trace_mul_comm, Matrix.mul_assoc]