We formalize the theory of subresultants and the subresultant polynomial remainder sequence as described by Brown and Traub. As a result, we obtain efficient certified algorithms for computing the resultant and the greatest common divisor of polynomials.
|Number of pages||28|
|Journal||Archive of Formal Proofs|
|Publication status||Published - 6 Apr 2017|