feat: port Data.Real.CauSeqCompletion (#1469)

Unreverts #1440 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
leanprover-community · Jan 13, 2023 · d4e2fbc · d4e2fbc
1 parent 64e7042
commit d4e2fbc
Show file tree

Hide file tree

Showing 2 changed files with 467 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -340,6 +340,7 @@ import Mathlib.Data.Rat.Lemmas
 import Mathlib.Data.Rat.Order
 import Mathlib.Data.Rat.Sqrt
 import Mathlib.Data.Real.CauSeq
+import Mathlib.Data.Real.CauSeqCompletion
 import Mathlib.Data.Rel
 import Mathlib.Data.Semiquot
 import Mathlib.Data.Set.Accumulate