mathlib documentation

algebra.quadratic_discriminant

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

Main statements

Tags

polynomial, quadratic, discriminant, root

def discrim {R : Type u_1} [ring R] :
R → R → R → R

Discriminant of a quadratic

Equations
theorem quadratic_eq_zero_iff_discrim_eq_square {R : Type u_1} [integral_domain R] {a b c : R} (h2 : 2 0) (ha : a 0) (x : R) :
(a * x) * x + b * x + c = 0 discrim a b c = ((2 * a) * x + b) ^ 2

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

theorem quadratic_ne_zero_of_discrim_ne_square {R : Type u_1} [integral_domain R] {a b c : R} (h2 : 2 0) (ha : a 0) (h : ∀ (s : R), discrim a b c s * s) (x : R) :
(a * x) * x + b * x + c 0

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

theorem quadratic_eq_zero_iff {K : Type u_1} [field K] [invertible 2] {a b c : K} (ha : a 0) {s : K} (h : discrim a b c = s * s) (x : K) :
(a * x) * x + b * x + c = 0 x = (-b + s) / 2 * a x = (-b - s) / 2 * a

Roots of a quadratic

theorem exists_quadratic_eq_zero {K : Type u_1} [field K] [invertible 2] {a b c : K} :
a 0(∃ (s : K), discrim a b c = s * s)(∃ (x : K), (a * x) * x + b * x + c = 0)

A quadratic has roots if its discriminant has square roots

theorem quadratic_eq_zero_iff_of_discrim_eq_zero {K : Type u_1} [field K] [invertible 2] {a b c : K} (ha : a 0) (h : discrim a b c = 0) (x : K) :
(a * x) * x + b * x + c = 0 x = -b / 2 * a

Root of a quadratic when its discriminant equals zero

theorem discrim_le_zero {K : Type u_1} [linear_ordered_field K] {a b c : K} :
(∀ (x : K), 0 (a * x) * x + b * x + c)discrim a b c 0

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

theorem discrim_lt_zero {K : Type u_1} [linear_ordered_field K] {a b c : K} :
a 0(∀ (x : K), 0 < (a * x) * x + b * x + c)discrim a b c < 0

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.