Documentation

Mathlib.Algebra.QuadraticDiscriminant

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] (a : R) (b : R) (c : R) :
R

Discriminant of a quadratic

Equations
Instances For
    @[simp]
    theorem discrim_neg {R : Type u_1} [Ring R] (a : R) (b : R) (c : R) :
    discrim (-a) (-b) (-c) = discrim a b c
    theorem discrim_eq_sq_of_quadratic_eq_zero {R : Type u_1} [CommRing R] {a : R} {b : R} {c : R} {x : R} (h : a * (x * x) + b * x + c = 0) :
    discrim a b c = (2 * a * x + b) ^ 2
    theorem quadratic_eq_zero_iff_discrim_eq_sq {R : Type u_1} [CommRing R] {a : R} {b : R} {c : R} [NeZero 2] [NoZeroDivisors R] (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_sq {R : Type u_1} [CommRing R] {a : R} {b : R} {c : R} (h : ∀ (s : R), discrim a b c s ^ 2) (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] [NeZero 2] {a : K} {b : K} {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 equation.

    theorem exists_quadratic_eq_zero {K : Type u_1} [Field K] [NeZero 2] {a : K} {b : K} {c : K} (ha : a 0) (h : ∃ (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] [NeZero 2] {a : K} {b : K} {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} [LinearOrderedField K] {a : K} {b : K} {c : K} (h : ∀ (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_le_zero_of_nonpos {K : Type u_1} [LinearOrderedField K] {a : K} {b : K} {c : K} (h : ∀ (x : K), a * (x * x) + b * x + c 0) :
    discrim a b c 0
    theorem discrim_lt_zero {K : Type u_1} [LinearOrderedField K] {a : K} {b : K} {c : K} (ha : a 0) (h : ∀ (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.

    theorem discrim_lt_zero_of_neg {K : Type u_1} [LinearOrderedField K] {a : K} {b : K} {c : K} (ha : a 0) (h : ∀ (x : K), a * (x * x) + b * x + c < 0) :
    discrim a b c < 0