Session Factor_Algebraic_Polynomial
View
theory dependencies
View
document
View
outline
Theories
Polynomials.MPoly_Type
Polynomials.More_MPoly_Type
Polynomials.MPoly_Type_Univariate
Symmetric_Polynomials.Vieta
Symmetric_Polynomials.Symmetric_Polynomials
Power_Sum_Polynomials.Power_Sum_Polynomials_Library
Hermite_Lindemann.More_Multivariate_Polynomial_HLW
Well_Quasi_Orders.Least_Enum
Well_Quasi_Orders.Infinite_Sequences
Open_Induction.Restricted_Predicates
Well_Quasi_Orders.Almost_Full
Well_Quasi_Orders.Minimal_Elements
Well_Quasi_Orders.Minimal_Bad_Sequences
Well_Quasi_Orders.Almost_Full_Relations
Polynomials.Utils
Well_Quasi_Orders.Well_Quasi_Orders
Polynomials.Power_Products
Polynomials.More_Modules
Polynomials.MPoly_Type_Class
Poly_Connection
MPoly_Divide
Polynomials.MPoly_Type_Class_Ordered
Polynomials.Poly_Mapping_Finite_Map
Polynomials.MPoly_Type_Class_FMap
MPoly_Divide_Code
MPoly_Container
Multivariate_Resultant
Is_Int_To_Int
Roots_of_Algebraic_Poly
Roots_of_Algebraic_Poly_Impl
Roots_via_IA
Roots_of_Real_Complex_Poly
Factor_Complex_Poly
Factor_Real_Poly