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

The discriminant of a quadratic a*x*x + b*x + c is b*b - 4*a*c.

Main statements

• Roots of a quadratic can be written as (-b + s) / (2 * a) or (-b - s) / (2 * a), where s is the square root of the discriminant. • If the discriminant has no square root, then the corresponding quadratic has no root. • If a quadratic is always non-negative, then its discriminant is non-positive.

Tags

polynomial, quadratic, discriminant, root

discrim

Discriminant of a quadratic

quadratic_eq_zero_iff_discrim_eq_square

A quadratic has roots if and only if its discriminant equals some square.

quadratic_eq_zero_iff

Roots of a quadratic

exist_quadratic_eq_zero

A quadratic has roots if its discriminant has square roots

quadratic_eq_zero_iff_of_discrim_eq_zero

Root of a quadratic when its discriminant equals zero

quadratic_ne_zero_of_discrim_ne_square

A quadratic has no root if its discriminant has no square root.

discriminant_le_zero

If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive

discriminant_lt_zero

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.