no goals
m : Type ?u.55351
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ det M = ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, M (↑σ i) i
simp [det_apply, Units.smul_def]