diff options
| author | Cyril Cohen | 2018-04-17 17:00:15 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-04-18 10:49:18 +0200 |
| commit | 13479422b0286c86d0888e06aba112153ca6314d (patch) | |
| tree | 6b921cad503e12fcea8dc7cc136667a54ea86bf4 /mathcomp/real_closed/descr | |
| parent | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (diff) | |
Moving real_closed to another repo
Diffstat (limited to 'mathcomp/real_closed/descr')
| -rw-r--r-- | mathcomp/real_closed/descr | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/mathcomp/real_closed/descr b/mathcomp/real_closed/descr deleted file mode 100644 index b51ecf9..0000000 --- a/mathcomp/real_closed/descr +++ /dev/null @@ -1,7 +0,0 @@ -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. |