English
If P is monic and splits over RingHom.id, then the constant term equals (-1)^{natDegree} times the product of the roots.
Русский
Если P моническое и распадается над RingHom.id, то константный коэффициент равен (-1)^{natDegree} умножить на произведение корней.
LaTeX
$$$P.Monic \land P.Splits (RingHom.id\ K) \Rightarrow coeff\ P\ 0 = (-1)^{P.natDegree} \cdot P.roots.prod$$$
Lean4
/-- If `P` is a monic polynomial that splits, then `coeff P 0` equals the product of the roots. -/
theorem coeff_zero_eq_prod_roots_of_monic_of_splits {P : K[X]} (hmo : P.Monic) (hP : P.Splits (RingHom.id K)) :
coeff P 0 = (-1) ^ P.natDegree * P.roots.prod :=
by
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
rw [coeff_zero_eq_eval_zero, eval_multiset_prod, Multiset.map_map]
simp_rw [Function.comp_apply, eval_sub, eval_X, zero_sub, eval_C]
simp only [splits_iff_card_roots.1 hP, Multiset.prod_map_neg]
