# The Solution of a Cubic #

This file proves Theorem 37 from the 100 Theorems List.

In this file, we give the solutions to the cubic equation a * x^3 + b * x^2 + c * x + d = 0 over a field K that has characteristic neither 2 nor 3, that has a third primitive root of unity, and in which certain other quantities admit square and cube roots.

This is based on the Cardano's Formula.

## Main statements #

• cubic_eq_zero_iff : gives the roots of the cubic equation where the discriminant p = 3 * a * c - b^2 is nonzero.
• cubic_eq_zero_iff_of_p_eq_zero : gives the roots of the cubic equation where the discriminant equals zero.

## References #

Originally ported from Isabelle/HOL. The original file was written by Amine Chaieb.

## Tags #

polynomial, cubic, root

theorem Theorems100.cube_root_of_unity_sum {K : Type u_1} [] {ω : K} (hω : ) :
1 + ω + ω ^ 2 = 0
theorem Theorems100.cubic_basic_eq_zero_iff {K : Type u_1} [] {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} (hω : ) (hp_nonzero : p 0) (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
x ^ 3 + 3 * p * x - 2 * q = 0 x = s - t x = s * ω - t * ω ^ 2 x = s * ω ^ 2 - t * ω

The roots of a monic cubic whose quadratic term is zero and whose discriminant is nonzero.

theorem Theorems100.cubic_monic_eq_zero_iff {K : Type u_1} [] (b : K) (c : K) (d : K) {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} [] [] (hω : ) (hp : p = (3 * c - b ^ 2) / 9) (hp_nonzero : p 0) (hq : q = (9 * b * c - 2 * b ^ 3 - 27 * d) / 54) (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
x ^ 3 + b * x ^ 2 + c * x + d = 0 x = s - t - b / 3 x = s * ω - t * ω ^ 2 - b / 3 x = s * ω ^ 2 - t * ω - b / 3

Roots of a monic cubic whose discriminant is nonzero.

theorem Theorems100.cubic_eq_zero_iff {K : Type u_1} [] (a : K) (b : K) (c : K) (d : K) {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} [] [] (ha : a 0) (hω : ) (hp : p = (3 * a * c - b ^ 2) / (9 * a ^ 2)) (hp_nonzero : p 0) (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 x = s - t - b / (3 * a) x = s * ω - t * ω ^ 2 - b / (3 * a) x = s * ω ^ 2 - t * ω - b / (3 * a)

The Solution of Cubic. The roots of a cubic polynomial whose discriminant is nonzero.

theorem Theorems100.cubic_eq_zero_iff_of_p_eq_zero {K : Type u_1} [] (a : K) (b : K) (c : K) (d : K) {ω : K} {q : K} {s : K} [] [] (ha : a 0) (hω : ) (hpz : 3 * a * c - b ^ 2 = 0) (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hs3 : s ^ 3 = 2 * q) (x : K) :
a * x ^ 3 + b * x ^ 2 + c * x + d = 0 x = s - b / (3 * a) x = s * ω - b / (3 * a) x = s * ω ^ 2 - b / (3 * a)

the solution of the cubic equation when p equals zero.