Polynomial Factorization

Title:	Polynomial Factorization
Authors:	René Thiemann and Akihisa Yamada
Submission date:	2016-01-29
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 square-free 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 primality-testing and prime-factorization algorithms for integers.
BibTeX:	@article{Polynomial_Factorization-AFP, author = {René Thiemann and Akihisa Yamada}, title = {Polynomial Factorization}, journal = {Archive of Formal Proofs}, month = jan, year = 2016, note = {\url{http://isa-afp.org/entries/Polynomial_Factorization.html}, Formal proof development}, ISSN = {2150-914x}, }
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
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.

Proof outline
Proof document

Browse theories

Download this entry