Session Count_Complex_Roots

Theories

• HOL-Computational_Algebra.Fraction_Field
• HOL-Computational_Algebra.Normalized_Fraction
• HOL-Computational_Algebra.Polynomial_Factorial
• HOL-Computational_Algebra.Fundamental_Theorem_Algebra
• Winding_Number_Eval.Missing_Topology
• Sturm_Tarski.PolyMisc
• HOL-Computational_Algebra.Field_as_Ring
• Sturm_Tarski.Sturm_Tarski
• Budan_Fourier.BF_Misc
• Winding_Number_Eval.Missing_Algebraic
• Winding_Number_Eval.Missing_Transcendental
• Polynomial_Interpolation.Ring_Hom
• Polynomial_Interpolation.Missing_Unsorted
• Polynomial_Interpolation.Missing_Polynomial
• Polynomial_Interpolation.Ring_Hom_Poly
• CC_Polynomials_Extra
• Winding_Number_Eval.Missing_Analysis
• Winding_Number_Eval.Cauchy_Index_Theorem
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• HOL-Eisbach.Eisbach_Tools
• Winding_Number_Eval.Winding_Number_Eval
• Extended_Sturm
• Budan_Fourier.Sturm_Multiple_Roots
• Count_Line
• Count_Half_Plane
• Count_Circle
• Count_Rectangle
• Count_Complex_Roots
• Count_Complex_Roots_Examples