English
Vieta’s formula for a polynomial p over an integral domain with as many roots as its degree: if p ∈ R[X], p.roots has cardinality natDegree(p), and k ≤ natDegree(p), then p.coeff k = p.leadingCoeff · (−1)^{natDegree(p)−k} · (p.roots.esymm (natDegree(p)−k)).
Русский
Формула Виета для полинома p над целочисленным доменом: если число корней p равно natDegree(p) и при этом 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), $$\n\ t\\text{ при } p.roots.card = p.natDegree \text{ и } k \\le p.natDegree. $$$$
Lean4
/-- Vieta's formula for the coefficients and the roots of a polynomial over an integral domain
with as many roots as its degree. -/
theorem _root_.Polynomial.coeff_eq_esymm_roots_of_card [IsDomain R] {p : R[X]}
(hroots : Multiset.card p.roots = p.natDegree) {k : ℕ} (h : k ≤ p.natDegree) :
p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k) :=
by
conv_lhs => rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
rw [coeff_C_mul, mul_assoc]; congr
have : k ≤ card (roots p) := by rw [hroots]; exact h
convert p.roots.prod_X_sub_C_coeff this using 3 <;> rw [hroots]
