
Polynomial
Factorization
Title: 
Polynomial Factorization 
Authors:

RenĂ© Thiemann and
Akihisa Yamada

Submission date: 
20160129 
Abstract: 
Based on existing libraries for polynomial interpolation and matrices,
we formalized several factorization algorithms for polynomials, including
Kronecker's algorithm for integer polynomials,
Yun's squarefree factorization algorithm for field polynomials, and
Berlekamp's algorithm for polynomials over finite fields.
By combining the last one with Hensel's lifting,
we derive an efficient factorization algorithm for the integer polynomials,
which is then lifted for rational polynomials by mechanizing Gauss' lemma.
Finally, we assembled a combined factorization algorithm for rational polynomials,
which combines all the mentioned algorithms and additionally uses the explicit formula for roots
of quadratic polynomials and a rational root test.
As side products, we developed division algorithms for polynomials over integral domains,
as well as primalitytesting and primefactorization algorithms for integers. 
BibTeX: 
@article{Polynomial_FactorizationAFP,
author = {RenĂ© Thiemann and Akihisa Yamada},
title = {Polynomial Factorization},
journal = {Archive of Formal Proofs},
month = jan,
year = 2016,
note = {\url{https://isaafp.org/entries/Polynomial_Factorization.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Partial_Function_MR, Polynomial_Interpolation, Show, Sqrt_Babylonian 
Used by: 
Amicable_Numbers, Dirichlet_Series, Functional_Ordered_Resolution_Prover, Gaussian_Integers, Jordan_Normal_Form, Knuth_Bendix_Order, Linear_Recurrences, Perron_Frobenius, Power_Sum_Polynomials, Subresultants 
