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^2is nonzero.
cubic_eq_zero_iff_of_p_eq_zero: gives the roots of the cubic equation where the discriminant equals zero.
Originally ported from Isabelle/HOL. The original file was written by Amine Chaieb.
polynomial, cubic, root
The roots of a monic cubic whose quadratic term is zero and whose discriminant is nonzero.
Roots of a monic cubic whose discriminant is nonzero.
The Solution of Cubic. The roots of a cubic polynomial whose discriminant is nonzero.
the solution of the cubic equation when p equals zero.