English
Let R be a commutative domain. For p(X) = a X^2 + b X + c with roots x1, x2 in R, one has c = a x1 x2.
Русский
Пусть R — коммутативная доменная кольцевая область. Для квадратного многочлена p(X) = aX^2 + bX + c с корнями x1, x2 в R выполняется c = a x1 x2.
LaTeX
$$$$\\text{Let } a,b,c\\in R \\text{ and } x_1,x_2\\in R.\\; (aX^2+bX+c)\\text{ has roots } x_1,x_2 \\;\\Rightarrow\\; c=a\\,x_1x_2. $$$$
Lean4
/-- **Vieta's formula** for quadratics. -/
theorem eq_mul_mul_of_roots_quadratic_eq_pair [CommRing R] [IsDomain R] {a b c x1 x2 : R}
(hroots : (C a * X ^ 2 + C b * X + C c).roots = { x1, x2 }) : c = a * x1 * x2 :=
by
let p : R[X] := C a * X ^ 2 + C b * X + C c
have hp_natDegree : p.natDegree = 2 :=
le_antisymm natDegree_quadratic_le (by convert p.card_roots'; rw [hroots, Multiset.card_pair])
have hp_roots_card : p.roots.card = p.natDegree := by rw [hp_natDegree, hroots, Multiset.card_pair]
simpa [leadingCoeff, hp_natDegree, p, hroots, mul_assoc, add_comm x1] using
coeff_eq_esymm_roots_of_card hp_roots_card (k := 0) (by simp [hp_natDegree])
