English
Let R be a commutative domain. For a quadratic p(X) = a X^2 + b X + c with a ≠ 0, the roots are x1,x2 in R iff b = -a(x1+x2) and c = a x1 x2.
Русский
Пусть R — коммутативная доменная область. Для квадратика p(X)=aX^2+bX+c с a ≠ 0 корни x1,x2 в R существуют тогда и только тогда, когда b = -a(x1+x2) и c = a x1 x2.
LaTeX
$$$$a\\neq 0 \\;\\wedge\\; p(X)=aX^2+bX+c \\text{ has roots } x_1,x_2 \\iff b=-a(x_1+x_2) \\wedge c=a x_1 x_2.$$$$
Lean4
/-- **Vieta's formula** for quadratics as an iff. -/
theorem roots_quadratic_eq_pair_iff_of_ne_zero [CommRing R] [IsDomain R] {a b c x1 x2 : R} (ha : a ≠ 0) :
(C a * X ^ 2 + C b * X + C c).roots = { x1, x2 } ↔ b = -a * (x1 + x2) ∧ c = a * x1 * x2 :=
have roots_of_ne_zero_of_vieta (hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2) :
(C a * X ^ 2 + C b * X + C c).roots = { x1, x2 } :=
by
suffices C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)
by
have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]
simpa [hvieta.1, hvieta.2] using by ring
⟨fun h => ⟨eq_neg_mul_add_of_roots_quadratic_eq_pair h, eq_mul_mul_of_roots_quadratic_eq_pair h⟩,
roots_of_ne_zero_of_vieta⟩
