package coq-corn
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Install
Dune Dependency
Authors
-
EEvgeny Makarov
-
RRobbert Krebbers
-
EEelis van der Weegen
-
BBas Spitters
-
JJelle Herold
-
RRussell O'Connor
-
CCezary Kaliszyk
-
DDan Synek
-
LLuís Cruz-Filipe
-
MMilad Niqui
-
IIris Loeb
-
HHerman Geuvers
-
RRandy Pollack
-
FFreek Wiedijk
-
JJan Zwanenburg
-
DDimitri Hendriks
-
HHenk Barendregt
-
MMariusz Giero
-
RRik van Ginneken
-
DDimitri Hendriks
-
SSébastien Hinderer
-
BBart Kirkels
-
PPierre Letouzey
-
LLionel Mamane
-
NNickolay Shmyrev
-
VVincent Semeria
Maintainers
Sources
sha512=cd61c8314fcbec3b38429e94c77ff76caccfb38cbfbc95faf9bbe127f86756299d9744a288a36c4cf9c02e0a8701e57491eab0eab44747458bcbc021e8f3b408
Description
CoRN 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
-
Exact Real Computation
Fast verified computation inside Coq. This includes: real numbers, functions, integrals, graphs of functions, differential equations.
Tags
category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology category:Mathematics/Exact Real computation keyword:constructive mathematics keyword:algebra keyword:real calculus keyword:real numbers keyword:Fundamental Theorem of Algebra logpath:CoRN date:2023-10-16Published: 17 Oct 2023
Dependencies (2)
- coq-bignums
-
coq-math-classes
>= "8.8.1"
Dev Dependencies (1)
-
coq
(>= "8.14" & < "8.19~") | (= "dev")
Used by
None
Conflicts
None