Session Hermite_Lindemann
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Adhoc_Overloading
File ‹adhoc_overloading.ML›
HOL-Library.Monad_Syntax
Polynomial_Interpolation.Ring_Hom
Polynomial_Interpolation.Missing_Unsorted
Polynomial_Interpolation.Missing_Polynomial
Polynomial_Interpolation.Ring_Hom_Poly
Polynomial_Interpolation.Divmod_Int
Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
Polynomial_Interpolation.Is_Rat_To_Rat
Polynomial_Interpolation.Newton_Interpolation
HOL-Computational_Algebra.Field_as_Ring
Polynomial_Factorization.Missing_Polynomial_Factorial
Polynomial_Factorization.Gauss_Lemma
Polynomial_Factorization.Polynomial_Divisibility
Containers.Containers_Auxiliary
Matrix.Utility
Polynomial_Factorization.Missing_List
Polynomial_Factorization.Missing_Multiset
Berlekamp_Zassenhaus.More_Missing_Multiset
HOL-Combinatorics.List_Permutation
HOL-Algebra.Divisibility
Berlekamp_Zassenhaus.Unique_Factorization
Jordan_Normal_Form.Missing_Misc
Jordan_Normal_Form.Missing_Ring
Jordan_Normal_Form.Conjugate
Jordan_Normal_Form.Matrix
Jordan_Normal_Form.Gauss_Jordan_Elimination
Jordan_Normal_Form.Column_Operations
Jordan_Normal_Form.Determinant
Subresultants.More_Homomorphisms
Berlekamp_Zassenhaus.Unique_Factorization_Poly
Polynomial_Factorization.Order_Polynomial
Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Polynomial_Factorization.Square_Free_Factorization
Algebraic_Numbers.Algebraic_Numbers_Prelim
Subresultants.Resultant_Prelim
Algebraic_Numbers.Bivariate_Polynomials
Algebraic_Numbers.Resultant
Algebraic_Numbers.Algebraic_Numbers
Algebraic_Integer_Divisibility
Algebraic_Numbers.Min_Int_Poly
Power_Sum_Polynomials.Power_Sum_Polynomials_Library
More_Polynomial_HLW
More_Min_Int_Poly
Complex_Lexorder
More_Multivariate_Polynomial_HLW
More_Algebraic_Numbers_HLW
Misc_HLW
Hermite_Lindemann