Vieta's Formula for polynomial of small degrees.

theorem Polynomial.eq_quadratic_of_degree_le_two {R : Type u_1} [Semiring R] {p : Polynomial R} (hp : p.degree ≤ 2) : p = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

theorem Polynomial.eq_neg_mul_add_of_roots_quadratic_eq_pair {R : Type u_1} [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)

Vieta's formula for quadratics.

theorem Polynomial.eq_mul_mul_of_roots_quadratic_eq_pair {R : Type u_1} [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

Vieta's formula for quadratics.

theorem Polynomial.eq_neg_mul_add_of_aroots_quadratic_eq_pair {T : Type u_2} {S : Type u_3} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {a b c : T} {x1 x2 : S} (haroots : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2}) : (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)

Vieta's formula for quadratics (aroots version).

theorem Polynomial.eq_mul_mul_of_aroots_quadratic_eq_pair {T : Type u_2} {S : Type u_3} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {a b c : T} {x1 x2 : S} (haroots : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2}) : (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Vieta's formula for quadratics (aroots version).

theorem Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero {R : Type u_1} [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

Vieta's formula for quadratics as an iff.

theorem Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero {T : Type u_2} {S : Type u_3} [CommRing T] [CommRing S] [IsDomain S] [Algebra T S] {a b c : T} {x1 x2 : S} (ha : (algebraMap T S) a ≠ 0) : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2} ↔ (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Vieta's formula for quadratics as an iff (aroots version).

theorem Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero' {R : Type u_1} [Field R] {a b c x1 x2 : R} (ha : a ≠ 0) : (C a * X ^ 2 + C b * X + C c).roots = {x1, x2} ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a

Vieta's formula for quadratics as an iff (Field version).

theorem Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero' {T : Type u_2} {S : Type u_3} [CommRing T] [Field S] [Algebra T S] {a b c : T} {x1 x2 : S} (ha : (algebraMap T S) a ≠ 0) : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2} ↔ x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a

Vieta's formula for quadratics as an iff (aroots, Field version).