no goals
m : Type ?u.1375840
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix n n R
⊢ det (-A) = (-1) ^ Fintype.card n * det A
rw [← det_smul, neg_one_smul]