Solving Cubic and Quartic Equations

 

Title: Solving Cubic and Quartic Equations
Author: René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2021-09-03
Abstract:

We formalize Cardano's formula to solve a cubic equation $$ax^3 + bx^2 + cx + d = 0,$$ as well as Ferrari's formula to solve a quartic equation. We further turn both formulas into executable algorithms based on the algebraic number implementation in the AFP. To this end we also slightly extended this library, namely by making the minimal polynomial of an algebraic number executable, and by defining and implementing $n$-th roots of complex numbers.

BibTeX:
@article{Cubic_Quartic_Equations-AFP,
  author  = {René Thiemann},
  title   = {Solving Cubic and Quartic Equations},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Cubic_Quartic_Equations.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Algebraic_Numbers, Complex_Geometry
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.