no goals
ι : Type ?u.25998
m : Type u_2
n : Type u_3
p : Type ?u.26007
α : Type ?u.26010
R : Type u_1
S : Type ?u.26016
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype p
inst✝¹ : AddCommMonoid R
inst✝ : CommSemigroup R
A : Matrix m n R
B : Matrix n m R
⊢ trace (A ⬝ B) = trace (B ⬝ A)
rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]