package coq-mathcomp-real-closed

You can search for identifiers within the package.

in-package search v0.2.0

Mathematical Components Library on real closed fields

Install

Dune Dependency

github.com Edit opam file Versions (12)

Authors

Maintainers

C

Cyril Cohen <cyril.cohen@inria.fr>

Sources

2.0.3.tar.gz

sha256=d8399b22da69ceda55db12b420b24066871f453ae37e9b206e94c95e5d3761d5

Description

This library contains definitions and theorems about real closed fields, with a construction of the real closure and the algebraic closure (including a proof of the fundamental theorem of algebra). It also contains a proof of decidability of the first order theory of real closed field, through quantifier elimination.

Published: 10 May 2025

Dependencies (7)

coq-mathcomp-bigenough >= "1.0.0"
coq-mathcomp-field
coq-mathcomp-algebra
coq-mathcomp-ssreflect >= "2.2.0" & < "2.5~"
coq >= "8.18" & < "9.1~"
coq-core >= "9.0" & < "9.1~"
coq >= "8.18" & < "8.21~"

Dev Dependencies

None

Used by (5)

Conflicts