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 + c is
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
s is 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.
polynomial, quadratic, discriminant, root
Discriminant of a quadratic
A quadratic has roots if and only if its discriminant equals some square.
A quadratic has no root if its discriminant has no square root.
A quadratic has roots if its discriminant has square roots
Root of a quadratic when its discriminant equals zero
If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive
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.