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.
• discrim_le_zero_of_nonpos, discrim_lt_zero, discrim_lt_zero_of_neg: versions of this statement with other inequalities.

Tags

polynomial, quadratic, discriminant, root

def discrim {R : Type u_1} [Ring R] (a b c : R) : R

Discriminant of a quadratic

Equations

• discrim a b c = b ^ 2 - 4 * a * c

@[simp]

theorem discrim_neg {R : Type u_1} [Ring R] (a b 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 b c 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 b 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 b 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 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 equation.

theorem exists_quadratic_eq_zero {K : Type u_1} [Field K] [NeZero 2] {a b 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 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_eq_zero_of_existsUnique {K : Type u_1} [Field K] [NeZero 2] {a b c : K} (ha : a ≠ 0) (h : ∃! x : K, a * (x * x) + b * x + c = 0) : discrim a b c = 0

theorem discrim_eq_zero_iff {K : Type u_1} [Field K] [NeZero 2] {a b c : K} (ha : a ≠ 0) : discrim a b c = 0 ↔ ∃! x : K, a * (x * x) + b * x + c = 0

theorem discrim_le_zero {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b 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} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b 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} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b 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} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a b c : K} (ha : a ≠ 0) (h : ∀ (x : K), a * (x * x) + b * x + c < 0) : discrim a b c < 0