Library

The library includes the following parts:

• Algebraic Hierarchy
  • An axiomatic formalization of the most common algebraic structures, including setoids, monoids, groups, rings, fields, ordered fields, rings of polynomials, real and complex numbers
    
• Model of the Real Numbers
  • Construction of a concrete real number structure satisfying the previously defined axioms
• Fundamental Theorem of Algebra
  • A proof that every non-constant polynomial on the complex plane has at least one root
• Real Calculus
  • A collection of elementary results on real analysis, including continuity, differentiability, integration, Taylor's theorem and the Fundamental Theorem of Calculus
• Metric Spaces
  • A theory of metric spaces. Includes product metrics, complete metrics, finite enumeration, compact sets.
• Effective Real Numbers
  • An effective implementation of real numbers for computing within Coq.