no goals
m : Type u_1
n : Type ?u.903620
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ det (M ⬝ N ⬝ P) = det (M ⬝ P ⬝ N)
rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]