case inl
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_1
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))

case inr
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_1
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))
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_1
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) (charpoly A)
⊢ trace A = Multiset.sum (roots (charpoly A))
cases' isEmpty_or_nonempty n with h
no goals
case inl
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_1
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))
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]
no goals
case inr
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_1
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))
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)]