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