nextCoeff_eq_neg_sum_roots_of_monic_of_splits

English

For a monic polynomial that splits, the nextCoeff equals the negative sum of the roots.

Русский

Для монического полинома, распадающегося, следующий коэффициент равен минусу суммы корней.

LaTeX

$$$P.Monic \Rightarrow P.nextCoeff = -\sum P.roots$$$

Lean4

/-- If `P` is a monic polynomial that splits, then `P.nextCoeff` equals the negative of the sum
of the roots. -/
theorem nextCoeff_eq_neg_sum_roots_of_monic_of_splits {P : K[X]} (hmo : P.Monic) (hP : P.Splits (RingHom.id K)) :
    P.nextCoeff = -P.roots.sum :=
  by
  nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
  rw [Monic.nextCoeff_multiset_prod _ _ fun a ha => _]
  · simp_rw [nextCoeff_X_sub_C, Multiset.sum_map_neg']
  · simp only [monic_X_sub_C, implies_true]

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