English
For a polynomial p over a field F that splits, with p.Splits (RingHom.id F), and for k ≤ natDegree(p), the same formula as above holds: p.coeff k = p.leadingCoeff · (−1)^{natDegree(p)−k} · p.roots.esymm (natDegree(p)−k).
Русский
Для многочлена p над полем F, который раскладывается (p.Splits (RingHom.id F)), при k ≤ natDegree(p) выполняется та же формула: p.coeff k = leadingCoeff(p) · (−1)^{natDegree(p)−k} · esymm(p.roots, natDegree(p)−k).
LaTeX
$$$$ p.coeff\_k = p.leadingCoeff \\cdot (-1)^{p.natDegree - k} \\cdot p.roots.esymm (p.natDegree - k). $$$$
Lean4
/-- Vieta's formula for split polynomials over a field. -/
theorem _root_.Polynomial.coeff_eq_esymm_roots_of_splits {F} [Field F] {p : F[X]} (hsplit : p.Splits (RingHom.id F))
{k : ℕ} (h : k ≤ p.natDegree) :
p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k) :=
Polynomial.coeff_eq_esymm_roots_of_card (splits_iff_card_roots.1 hsplit) h
