Session Factor_Algebraic_Polynomial

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