aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/real_closed/descr
blob: b51ecf9b44020334bb41d28a79d3a8f9c5c6f021 (plain)
1
2
3
4
5
6
7
Mathematical Components Library on real closed fields

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.