Session Modular_arithmetic_LLL_and_HNF_algorithms

Theories

• HOL-Library.Adhoc_Overloading
  • File ‹adhoc_overloading.ML›
• HOL-Library.Monad_Syntax
• Containers.Containers_Auxiliary
• Containers.Containers_Generator
  • File ‹containers_generator.ML›
• Containers.Collection_Enum
  • File ‹cenum_generator.ML›
• Deriving.Equality_Generator
  • File ‹equality_generator.ML›
• Deriving.Equality_Instances
• Containers.Collection_Eq
  • File ‹ceq_generator.ML›
• Containers.Equal
• Containers.DList_Set
• Containers.List_Fusion
• HOL-Library.Char_ord
• Containers.Lexicographic_Order
• Containers.Extend_Partial_Order
• Containers.Set_Linorder
• Deriving.Comparator
• Deriving.Comparator_Generator
  • File ‹comparator_generator.ML›
• Deriving.Compare
  • File ‹compare_code.ML›
• Deriving.Compare_Generator
  • File ‹compare_generator.ML›
• Deriving.Compare_Instances
• Containers.Collection_Order
  • File ‹ccompare_generator.ML›
• HOL-Library.RBT_Impl
• Containers.RBT_ext
• Deriving.RBT_Comparator_Impl
• Containers.RBT_Mapping2
• Containers.RBT_Set2
• Containers.Closure_Set
• Containers.Set_Impl
  • File ‹set_impl_generator.ML›
• Jordan_Normal_Form.Matrix_IArray_Impl
• Matrix_Change_Row
• Matrix.Utility
• Polynomial_Factorization.Polynomial_Irreducibility
• Polynomial_Factorization.Square_Free_Factorization
• Polynomial_Factorization.Missing_List
• Polynomial_Factorization.Missing_Multiset
• Berlekamp_Zassenhaus.More_Missing_Multiset
• HOL-Combinatorics.List_Permutation
• HOL-Algebra.Divisibility
• Berlekamp_Zassenhaus.Unique_Factorization
• Polynomial_Factorization.Missing_Polynomial_Factorial
• Subresultants.More_Homomorphisms
• Berlekamp_Zassenhaus.Unique_Factorization_Poly
• Berlekamp_Zassenhaus.Poly_Mod
• Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
• Signed_Modulo
• Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
• Jordan_Normal_Form.Determinant_Impl
• Show.Shows_Literal
• Jordan_Normal_Form.Shows_Literal_Matrix
• Jordan_Normal_Form.Matrix_Impl
• Subresultants.Resultant_Prelim
• Algebraic_Numbers.Bivariate_Polynomials
• Algebraic_Numbers.Resultant
• Berlekamp_Zassenhaus.Sublist_Iteration
• Subresultants.Dichotomous_Lazard
• Subresultants.Coeff_Int
• Subresultants.Subresultant
• Subresultants.Subresultant_Gcd
• Sqrt_Babylonian.Log_Impl
• Cauchy.CauchysMeanTheorem
• Sqrt_Babylonian.NthRoot_Impl
• Sqrt_Babylonian.Sqrt_Babylonian
• Polynomial_Factorization.Explicit_Roots
• Polynomial_Interpolation.Improved_Code_Equations
• 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
• HOL-Library.RBT
• HOL-Library.AList
• HOL-Library.Mapping
• HOL-Library.RBT_Mapping
• 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
• Polynomial_Factorization.Rational_Factorization
• Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
• Jordan_Normal_Form.Matrix_Kernel
• Berlekamp_Zassenhaus.Chinese_Remainder_Poly
• Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
• Berlekamp_Zassenhaus.Berlekamp_Type_Based
• Berlekamp_Zassenhaus.Distinct_Degree_Factorization
• Berlekamp_Zassenhaus.Finite_Field_Factorization
• Berlekamp_Zassenhaus.Arithmetic_Record_Based
• Berlekamp_Zassenhaus.Matrix_Record_Based
• HOL-Library.Type_Length
• HOL-Library.Word
  • File ‹Tools/word_lib.ML›
  • File ‹Tools/smt_word.ML›
• 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
• HOL-Library.Signed_Division
• 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
• Berlekamp_Zassenhaus.Finite_Field_Record_Based
• Berlekamp_Zassenhaus.Karatsuba_Multiplication
• Berlekamp_Zassenhaus.Polynomial_Record_Based
• Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based
• Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based
• Berlekamp_Zassenhaus.Hensel_Lifting
• Berlekamp_Zassenhaus.Berlekamp_Hensel
• LLL_Basis_Reduction.Missing_Lemmas
• LLL_Basis_Reduction.Norms
• LLL_Basis_Reduction.Int_Rat_Operations
• LLL_Basis_Reduction.Gram_Schmidt_2
• Regular-Sets.Regular_Set
• Regular-Sets.Regular_Exp
• Regular-Sets.NDerivative
• HOL-Library.While_Combinator
• Regular-Sets.Equivalence_Checking
• Regular-Sets.Relation_Interpretation
• Regular-Sets.Regexp_Method
• Abstract-Rewriting.Seq
• Abstract-Rewriting.Abstract_Rewriting
• Abstract-Rewriting.SN_Orders
• Abstract-Rewriting.SN_Order_Carrier
• LLL_Basis_Reduction.LLL
• LLL_Basis_Reduction.List_Representation
• LLL_Basis_Reduction.More_IArray
• LLL_Basis_Reduction.Gram_Schmidt_Int
• LLL_Basis_Reduction.LLL_Impl
• LLL_Basis_Reduction.LLL_Certification
• Storjohann_Mod_Operation
• LLL_Basis_Reduction.LLL_Number_Bounds
• Storjohann
• Storjohann_Impl
• Uniqueness_Hermite
• Uniqueness_Hermite_JNF
• HNF_Mod_Det_Algorithm
• HNF_Mod_Det_Soundness
• LLL_Certification_via_HNF