14 search results for "tag:"category:Mathematics/Real Calculus and Topology""
-
coq-actuary
No documentation
Formalization of actuarial mathematics in Coq2.6MITUsed by 0 other packages11 Nov 2023 -
coq-coqtail
No documentation
Library of mathematical theorems tools proved inside the Coq8.20LGPL-3.0-onlyUsed by 0 other packages14 Jul 2024 -
coq-coquelicot
No documentation
A Coq formalization of real analysis compatible with the stard library3.4.4LGPL-3.0-or-laterUsed by 10 other packages30 Jul 2025 -
coq-corn
No documentation
The Coq Constructive Repository at Nijmegen8.20.0GPL-2.0Used by 0 other packages01 Feb 2025 -
coq-fourcolor-reals
No documentation
Interface for real numbers used in the Four Color Theorem1.4.1CECILL-BUsed by 2 other packages21 Apr 2025 -
coq-hol-light
No documentation
HOL-Light library in Coqlogpath:HOLLight date:2025-01-20 category:Mathematics/Arithmetic Number Theory/Miscellaneous category:Mathematics/Real Numbers category:Mathematics/Real Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendental3.0.0CeCILL-2.1Used by 0 other packages21 Jan 2025 -
coq-improper-integrals
No documentation
Additions to the coquelicot library for hling improper integrals0.1.0MITUsed by 0 other packages19 Apr 2018 -
coq-interval
No documentation
A Coq tactic for proving bounds on real-valued expressions automatically4.11.3CeCILL-CUsed by 8 other packages31 Jul 2025 -
coq-mathcomp-analysis
No documentation
An analysis library for mathematical componentscategory:Mathematics/Real Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Lau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis1.13.0CECILL-CUsed by 7 other packages19 Aug 2025 -
coq-num-analysis
No documentation
Numerical Analysis in Coq1.0.0LGPL-3.0-or-laterUsed by 0 other packages06 Sep 2022 -
coq-pi-agm
No documentation
Computing thouss or millions of digits of PI with arithmetic-geometric means1.2.8CECILL-BUsed by 0 other packages20 Jun 2024 -
coq-quantumlib
No documentation
Coq library for reasoning about quantum programs1.7.0MITUsed by 0 other packages29 Jul 2025 -
coq-topology
No documentation
General topology in Coq10.2.0LGPL-2.1-or-laterUsed by 0 other packages21 Aug 2023 -
rocq-pi-agm
No documentation
Computing thouss or millions of digits of PI with arithmetic-geometric means1.2.9CECILL-BUsed by 0 other packages14 Aug 2025