Session Berlekamp_Zassenhaus

Theories

• HOL-Number_Theory.Cong
• HOL-Number_Theory.Totient
• HOL-Number_Theory.Residues
• Finite_Field
• Arithmetic_Record_Based
• Word_Lib.More_Arithmetic
• Word_Lib.More_Divides
• Word_Lib.More_Bit_Ring
• Word_Lib.More_Word
• Word_Lib.Bit_Shifts_Infix_Syntax
• Word_Lib.Most_significant_bit
• Word_Lib.Least_significant_bit
• Word_Lib.Generic_set_bit
• Word_Lib.Bit_Comprehension
• Word_Lib.Signed_Division_Word
• Native_Word.Code_Target_Word_Base
• Native_Word.Word_Type_Copies
• Native_Word.Code_Int_Integer_Conversion
• Native_Word.Code_Target_Integer_Bit
• Native_Word.Uint32
• Native_Word.Uint64
• Native_Word.Code_Target_Int_Bit
• Finite_Field_Record_Based
• Matrix_Record_Based
• Matrix.Utility
• Polynomial_Factorization.Polynomial_Irreducibility
• Polynomial_Factorization.Square_Free_Factorization
• Polynomial_Factorization.Missing_List
• Polynomial_Factorization.Missing_Multiset
• More_Missing_Multiset
• Unique_Factorization
• Unique_Factorization_Poly
• Poly_Mod
• HOL-Types_To_Sets.Types_To_Sets
  • File ‹local_typedef.ML›
  • File ‹unoverloading.ML›
  • File ‹internalize_sort.ML›
  • File ‹unoverload_type.ML›
  • File ‹unoverload_def.ML›
• Poly_Mod_Finite_Field
• Karatsuba_Multiplication
• Polynomial_Record_Based
• Poly_Mod_Finite_Field_Record_Based
• Chinese_Remainder_Poly
• Berlekamp_Type_Based
• Distinct_Degree_Factorization
• Finite_Field_Factorization
• Polynomial_Interpolation.Improved_Code_Equations
• Finite_Field_Factorization_Record_Based
• Hensel_Lifting
• Hensel_Lifting_Type_Based
• Berlekamp_Hensel
• Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
• Sqrt_Babylonian.Log_Impl
• Cauchy.CauchysMeanTheorem
• Sqrt_Babylonian.NthRoot_Impl
• Sqrt_Babylonian.Sqrt_Babylonian
• Polynomial_Factorization.Explicit_Roots
• Polynomial_Interpolation.Divmod_Int
• Polynomial_Interpolation.Is_Rat_To_Rat
• Polynomial_Interpolation.Newton_Interpolation
• Polynomial_Interpolation.Lagrange_Interpolation
• Polynomial_Interpolation.Neville_Aitken_Interpolation
• Polynomial_Interpolation.Polynomial_Interpolation
• Polynomial_Factorization.Prime_Factorization
• Polynomial_Factorization.Precomputation
• Polynomial_Factorization.Gauss_Lemma
• Polynomial_Factorization.Dvd_Int_Poly
• Polynomial_Factorization.Kronecker_Factorization
• Polynomial_Factorization.Rational_Root_Test
• Polynomial_Factorization.Gcd_Rat_Poly
• Show.Show_Poly
• Polynomial_Factorization.Rational_Factorization
• Square_Free_Int_To_Square_Free_GFp
• Suitable_Prime
• Efficient-Mergesort.Efficient_Sort
• Degree_Bound
• Mahler_Measure
• Factor_Bound
• Sublist_Iteration
• Reconstruction
• Code_Abort_Gcd
• Berlekamp_Zassenhaus
• Gcd_Finite_Field_Impl
• Square_Free_Factorization_Int
• Factorize_Int_Poly
• Factorize_Rat_Poly
• Factorization_External_Interface