Theorems · Theorem · ring theory

vieta_formula_quadratic

∀ {α : Type u_3} [inst : NonUnitalCommRing α] {b c x : α},
  x * x - b * x + c = 0 → ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with its roots. This particular version states that if we have a root x of a monic quadratic polynomial, then there is another root y such that x + y is negative the a_1 coefficient and x * y is the a_0 coefficient.

Defined in

Mathlib.Algebra.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

NonUnitalCommRing