R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nonempty n
M : Matrix n n R
⊢ ∑ i : n, diag M i = ∑ i : n, M i i
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nonempty n
M : Matrix n n R
⊢ trace M = -coeff (charpoly M) (Fintype.card n - 1)
rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
  prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]
no goals
R : Type u
inst✝⁴ : CommRing R
n G : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
α β : Type v
inst✝¹ : DecidableEq α
M✝ : Matrix n n R
inst✝ : Nonempty n
M : Matrix n n R
⊢ ∑ i : n, diag M i = ∑ i : n, M i i
simp_rw [diag_apply]