![[Jenkins]](/jenkins/static/ce11adf6/images/svgs/logo.svg){kind=logo}
Summary
- merge
- use new certified Berlekamp-Zassenhaus algorithm for algebraic numbers, remove old factorization oracle for Berlekamp-Hensel-Zassenhaus
- moved resultants from Algebraic-Numbers into Berlekamp-Zassenhaus (towards building dependence Poly-Factorization <- BZ <- Alg-Num)
| The file was modified | thys/Algebraic_Numbers/Algebraic_Number_Tests.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/ROOT (diff) |
| The file was modified | thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/Real_Roots.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/Show_Real_Precise.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/document/root.tex (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/Factor_Bound.thy (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.thy (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/ROOT (diff) |
| The file was modified | thys/Polynomial_Factorization/ROOT (diff) |
| The file was modified | thys/Polynomial_Factorization/Rational_Factorization.thy (diff) |
| The file was modified | thys/Polynomial_Factorization/document/root.tex (diff) |
| The file was removed | thys/Polynomial_Factorization/Berlekamp_Hensel_Factorization.thy |
| The file was removed | thys/Polynomial_Factorization/Factorization_Oracle.thy |
| The file was removed | thys/Polynomial_Factorization/Gauss_Jordan_Field.thy |
| The file was removed | thys/Polynomial_Factorization/Polynomial_Field.thy |
| The file was removed | thys/Polynomial_Factorization/Prime_Field.thy |
| The file was removed | thys/Polynomial_Factorization/Select_Berlekamp_Hensel_Factorization.thy |
| The file was removed | thys/Polynomial_Factorization/Select_External_Factorization.thy |
| The file was removed | thys/Polynomial_Factorization/Select_Hybrid_Factorization.thy |
| The file was removed | thys/Polynomial_Factorization/Select_Mathematica_Factorization.thy |
| The file was added | thys/Berlekamp_Zassenhaus/Binary_Exponentiation.thy |
| The file was added | thys/Berlekamp_Zassenhaus/Bivariate_Polynomials.thy |
| The file was added | thys/Berlekamp_Zassenhaus/Resultant.thy |
| The file was modified | thys/Algebraic_Numbers/Algebraic_Numbers.thy (diff) |
| The file was modified | thys/Algebraic_Numbers/ROOT (diff) |
| The file was modified | thys/Algebraic_Numbers/document/root.tex (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/Finite_Field.thy (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/ROOT (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy (diff) |
| The file was modified | thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy (diff) |
| The file was modified | thys/Polynomial_Interpolation/Ring_Hom.thy (diff) |
| The file was modified | thys/Polynomial_Interpolation/Ring_Hom_Poly.thy (diff) |
| The file was removed | thys/Algebraic_Numbers/Binary_Exponentiation.thy |
| The file was removed | thys/Algebraic_Numbers/Bivariate_Polynomials.thy |
| The file was removed | thys/Algebraic_Numbers/Resultant.thy |