[GOAL]
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) (charpoly A)
⊢ det A = Multiset.prod (roots (charpoly A))
[PROOFSTEP]
rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim A,
  Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split A.charpoly_monic hAps, ← mul_assoc, ← pow_two, pow_right_comm,
  neg_one_sq, one_pow, one_mul]
[GOAL]
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) (charpoly A)
⊢ trace A = Multiset.sum (roots (charpoly A))
[PROOFSTEP]
cases' isEmpty_or_nonempty n with h
[GOAL]
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) (charpoly A)
h : IsEmpty n
⊢ trace A = Multiset.sum (roots (charpoly A))
[PROOFSTEP]
rw [Matrix.trace, Fintype.sum_empty, Matrix.charpoly, det_eq_one_of_card_eq_zero (Fintype.card_eq_zero_iff.2 h),
  Polynomial.roots_one, Multiset.empty_eq_zero, Multiset.sum_zero]
[GOAL]
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) (charpoly A)
h✝ : Nonempty n
⊢ trace A = Multiset.sum (roots (charpoly A))
[PROOFSTEP]
rw [trace_eq_neg_charpoly_coeff, neg_eq_iff_eq_neg, ←
  Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split A.charpoly_monic hAps, nextCoeff, charpoly_natDegree_eq_dim,
  if_neg (Fintype.card_ne_zero : Fintype.card n ≠ 0)]
