no goals
R : Type ?u.18410
inst✝¹⁰ : CommRing R
M✝ : Type ?u.18416
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
M' : Type ?u.19001
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.19543
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M✝
A : Type u_2
inst✝³ : CommRing A
m : Type ?u.20027
n : Type u_1
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M N : Matrix n n A
⊢ det (M ⬝ N) = det (N ⬝ M)
rw [det_mul, det_mul, mul_comm]