trace_eq_sum_roots_charpoly_of_splits

English

If the characteristic polynomial splits over K, the trace equals the sum of the roots: trace(A) = charpoly(A).roots.sum.

Русский

Если характеристический полином раскладывается над K, след равен сумме корней: trace(A) = charpoly(A).roots.sum.

LaTeX

$$A.trace = A.charpoly.roots.sum$$

Lean4

theorem trace_eq_sum_roots_charpoly_of_splits (hAps : A.charpoly.Splits (RingHom.id K)) :
    A.trace = (Matrix.charpoly A).roots.sum :=
  by
  rcases isEmpty_or_nonempty n with h | _
  ·
    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]
  ·
    rw [trace_eq_neg_charpoly_nextCoeff, neg_eq_iff_eq_neg, ←
      Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits A.charpoly_monic hAps]

Похожие утверждения