eq_neg_mul_add_of_roots_quadratic_eq_pair

English

Let R be a commutative domain. For a quadratic p(X) = a X^2 + b X + c with roots x1, x2 in R, one has b = -a(x1 + x2).

Русский

Пусть R — коммутативная доменная кольцевая область. Для квадратного многочлена p(X) = aX^2 + bX + c с корнями x1, x2 в R выполняется b = -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\\; b=-a\\,(x_1+x_2).$$$$

Lean4

/-- **Vieta's formula** for quadratics. -/
theorem eq_neg_mul_add_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 }) : b = -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 := 1) (by simp [hp_natDegree])

Похожие утверждения