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} [Field K] {ω : K} (hω : IsPrimitiveRoot ω 3) : 1 + ω + ω ^ 2 = 0

theorem Theorems100.cubic_basic_eq_zero_iff {K : Type u_1} [Field K] {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} (hω : IsPrimitiveRoot ω 3) (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} [Field K] (b : K) (c : K) (d : K) {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} [Invertible 2] [Invertible 3] (hω : IsPrimitiveRoot ω 3) (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} [Field K] (a : K) (b : K) (c : K) (d : K) {ω : K} {p : K} {q : K} {r : K} {s : K} {t : K} [Invertible 2] [Invertible 3] (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3) (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} [Field K] (a : K) (b : K) (c : K) (d : K) {ω : K} {q : K} {s : K} [Invertible 2] [Invertible 3] (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3) (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.