Quadratic discriminants and roots of a quadratic #
This file defines the discriminant of a quadratic and gives the solution to a quadratic equation.
Main definition #
discrim a b c: the discriminant of a quadratic
a * x * x + b * x + cis
b * b - 4 * a * c.
Main statements #
quadratic_eq_zero_iff: roots of a quadratic can be written as
(-b + s) / (2 * a)or
(-b - s) / (2 * a), where
sis a square root of the discriminant.
quadratic_ne_zero_of_discrim_ne_sq: if the discriminant has no square root, then the corresponding quadratic has no root.
discrim_le_zero: if a quadratic is always non-negative, then its discriminant is non-positive.
discrim_lt_zero_of_neg: versions of this statement with other inequalities.
polynomial, quadratic, discriminant, root
If a polynomial of degree 2 is always positive, then its discriminant is negative, at least when the coefficient of the quadratic term is nonzero.