feat(library/data/real): define real numbers, prove they form a commutative ring

2015-05-26 12:05:53 +10:00 · 2015-05-26 12:05:53 +10:00 · 393cefcf97
commit 393cefcf97
parent 681f431d4b
3 changed files with 1243 additions and 0 deletions
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
--- a/library/data/real/default.lean
+++ b/library/data/real/default.lean
@ -0,0 +1,6 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Robert Y. Lewis
+-/
+import .basic
--- a/library/data/real/real.md
+++ b/library/data/real/real.md
@ -0,0 +1,6 @@
+data.real
+========
+
+The real numbers.
+
+* [basic](basic.lean) : the reals as a commutative ring