diff options
| author | Florent Hivert | 2018-09-11 19:35:26 +0200 |
|---|---|---|
| committer | Florent Hivert | 2018-09-11 19:35:26 +0200 |
| commit | 6b9e7f66db123a27c5ac7c52bebc67580940bfb6 (patch) | |
| tree | 0345c70096f1756a4109d217d89389b3b1c81eb4 /mathcomp | |
| parent | 692bb256df722bdf392578bd1f0e2a5eb3b468e9 (diff) | |
Fixes the doc of rat
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/rat.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 27f59f5..b56bc2a 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -11,8 +11,8 @@ 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 *) -(* n%:Q == explicit cast from int to rat, postfix notation for the *) -(* ratz constant *) +(* n%:Q == explicit cast from int to rat, ie. the specialization to *) +(* rationals of the generic ring morphism n%:~R *) (* numq r == numerator of (r : rat) *) (* denq r == denominator of (r : rat) *) (* x \is a Qint == x is an element of rat whose denominator is equal to 1 *) |