The Solution of a Cubic #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

theorem theorems_100.cube_root_of_unity_sum {K : Type u_1} [field K] [invertible 2] [invertible 3] {ω : K} (hω : is_primitive_root ω 3) :

1 + ω + ω ^ 2 = 0

source

theorem theorems_100.cubic_basic_eq_zero_iff {K : Type u_1} [field K] [invertible 2] [invertible 3] {ω p q r s t : K} (hω : is_primitive_root ω 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.

source

theorem theorems_100.cubic_monic_eq_zero_iff {K : Type u_1} [field K] [invertible 2] [invertible 3] (b c d : K) {ω p q r s t : K} (hω : is_primitive_root ω 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.

source

theorem theorems_100.cubic_eq_zero_iff {K : Type u_1} [field K] [invertible 2] [invertible 3] (a b c d : K) {ω p q r s t : K} (ha : a ≠ 0) (hω : is_primitive_root ω 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.

source

theorem theorems_100.cubic_eq_zero_iff_of_p_eq_zero {K : Type u_1} [field K] [invertible 2] [invertible 3] (a b c d : K) {ω q s : K} (ha : a ≠ 0) (hω : is_primitive_root ω 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.