### 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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Polynomial_Factorization

- Missing_List
- Missing_Multiset
- Precomputation
- Order_Polynomial
- Explicit_Roots
- Dvd_Int_Poly
- Missing_Polynomial_Factorial
- Gauss_Lemma
- Prime_Factorization
- Rational_Root_Test
- Kronecker_Factorization
- Polynomial_Divisibility
- Fundamental_Theorem_Algebra_Factorized
- Square_Free_Factorization
- Gcd_Rat_Poly
- Rational_Factorization

### Depends on

- Abstract Rewriting
- Light-weight Containers
- Gauss-Jordan Algorithm and Its Applications
- Executable Matrix Operations on Matrices of Arbitrary Dimensions
- Mutually Recursive Partial Functions
- Polynomial Interpolation
- Haskell’s Show Class in Isabelle/HOL
- Computing N-th Roots using the Babylonian Method
- Vector Spaces

### Used by

- Continued Fractions
- Fisher’s Inequality: Linear Algebraic Proof Techniques for Combinatorics
- Amicable Numbers
- A Formalization of Knuth–Bendix Orders
- Gaussian Integers
- Power Sum Polynomials
- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover
- Dirichlet Series
- Linear Recurrences
- Subresultants
- The Factorization Algorithm of Berlekamp and Zassenhaus
- Perron-Frobenius Theorem for Spectral Radius Analysis
- Matrices, Jordan Normal Forms, and Spectral Radius Theory

### Auto-related entries

- The Factorization Algorithm of Berlekamp and Zassenhaus

## Cite

×

Polynomial_Factorization-AFP

    @article{Polynomial_Factorization-AFP,
      author  = {René Thiemann and Akihisa Yamada},
      title   = {Polynomial Factorization},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Polynomial_Factorization.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016