diff --git a/library/data/real/real.md b/library/data/real/real.md index 2acde23a7..5e05818fd 100644 --- a/library/data/real/real.md +++ b/library/data/real/real.md @@ -1,8 +1,9 @@ data.real ======== -The real numbers. +The real numbers: classically, as a quotient type; constructively, as a setoid. * [basic](basic.lean) : the reals as a commutative ring (constructive) * [order](order.lean) : the reals as an ordered ring (constructive) -* [division](division.lean) : the reals as a discrete linear ordered field (classical) \ No newline at end of file +* [division](division.lean) : the reals as a discrete linear ordered field (classical) +* [complete](complete.lean) : the reals are Cauchy complete (classical) \ No newline at end of file