lean2/library/data/real/real.md

6 lines
No EOL
94 B
Markdown

data.real
========
The real numbers.
* [basic](basic.lean) : the reals as a commutative ring