diff options
| author | Cyril Cohen | 2018-09-12 13:53:56 +0200 |
|---|---|---|
| committer | GitHub | 2018-09-12 13:53:56 +0200 |
| commit | 278b9af169ce8bbac59a96f5f7136dc313b7474a (patch) | |
| tree | 0345c70096f1756a4109d217d89389b3b1c81eb4 | |
| parent | 692bb256df722bdf392578bd1f0e2a5eb3b468e9 (diff) | |
| parent | 6b9e7f66db123a27c5ac7c52bebc67580940bfb6 (diff) | |
Merge pull request #228 from hivert/docfix
Fixes the doc of rat
| -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 *) |