diff options
| author | Cyril Cohen | 2016-08-25 01:38:44 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2016-08-25 01:39:43 +0200 |
| commit | 2d824f394e8c3148e95b3374fb9903f6032ba3e6 (patch) | |
| tree | 6640dead8c6ee6147eebdc0c9e12bfa621787ced /mathcomp/algebra/rat.v | |
| parent | 933085b944ecef3d50de3c81444079c30c462ca9 (diff) | |
Enriched numClosedFieldType so that it factors a lot of theory from both complex and algC.
The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.
Diffstat (limited to 'mathcomp/algebra/rat.v')
| -rw-r--r-- | mathcomp/algebra/rat.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 9012291..9a38f5b 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -11,8 +11,6 @@ Require Import bigop ssralg div ssrnum ssrint. (* structure of archimedean, real field, with int and nat declared as closed *) (* subrings. *) (* rat == the type of rational number, with single constructor Rat *) -(* Rat p h == the element of type rat build from p a pair of integers and*) -(* h a proof of (0 < p.2) && coprime `|p.1| `|p.2| *) (* n%:Q == explicit cast from int to rat, postfix notation for the *) (* ratz constant *) (* numq r == numerator of (r : rat) *) |