no goals
m : Type u_1
n : Type ?u.899819
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 (N ⬝ (M ⬝ P))
rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]