diff options
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 *) |