no goals
m : Type ?u.1316454
n : Type u_2
inst✝⁸ : DecidableEq n
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq m
inst✝⁵ : Fintype m
R : Type v
inst✝⁴ : CommRing R
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ det (c • A) = c ^ Fintype.card n • det A
rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]