no goals
m : Type ?u.1307018
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
c : R
⊢ det (c • A) = det ((diagonal fun x => c) ⬝ A)
rw [smul_eq_diagonal_mul]
no goals
m : Type ?u.1307018
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
c : R
⊢ det (diagonal fun x => c) * det A = c ^ Fintype.card n * det A
simp [card_univ]