R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
⊢ det M = det (-1 • eval (↑(scalar n) 0) (X - ↑C M))
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
⊢ det M = (-1) ^ Fintype.card n * coeff (charpoly M) 0
rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]
no goals
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ M : Matrix n n R
⊢ det M = det (-1 • eval (↑(scalar n) 0) (X - ↑C M))
simp