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

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

source
theorem exists_le_mul_self {α : Type u_1} [linear_ordered_field α] (a : α) :
∃ (x : α), a ≤ x * x

source
theorem exists_lt_mul_self {α : Type u_1} [linear_ordered_field α] (a : α) :
∃ (x : α), a < x * x

source
def discrim {α : Type u_1} [linear_ordered_field α] [ring α] (a b c : α) :
α

Discriminant of a quadratic

Equations
source
theorem quadratic_eq_zero_iff_discrim_eq_square {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : a ≠ 0) (x : α) :
(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.

source
theorem quadratic_eq_zero_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : a ≠ 0) {s : α} (h : discrim a b c = s * s) (x : α) :
(a * x) * x + b * x + c = 0 ↔ x = (-b + s) / 2 * a ∨ x = (-b - s) / 2 * a

Roots of a quadratic

source
theorem exist_quadratic_eq_zero {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : a ≠ 0) (h : ∃ (s : α), discrim a b c = s * s) :
∃ (x : α), (a * x) * x + b * x + c = 0

A quadratic has roots if its discriminant has square roots

source
theorem quadratic_eq_zero_iff_of_discrim_eq_zero {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : a ≠ 0) (h : discrim a b c = 0) (x : α) :
(a * x) * x + b * x + c = 0 ↔ x = -b / 2 * a

Root of a quadratic when its discriminant equals zero

source
theorem quadratic_ne_zero_of_discrim_ne_square {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : a ≠ 0) (h : ∀ (s : α), discrim a b c ≠ s * s) (x : α) :
(a * x) * x + b * x + c ≠ 0

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

source
theorem discriminant_le_zero {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : ∀ (x : α), 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

source
theorem discriminant_lt_zero {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : a ≠ 0) (h : ∀ (x : α), 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.