feat: port Data.Real.EReal (#2501)

leanprover-community · Feb 28, 2023 · 127bbb2 · 127bbb2
1 parent 0ed2027
commit 127bbb2
Show file tree

Hide file tree

Showing 4 changed files with 1,262 additions and 3 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -657,6 +657,7 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.CauSeq
 import Mathlib.Data.Real.CauSeqCompletion
 import Mathlib.Data.Real.ENNReal
+import Mathlib.Data.Real.EReal
 import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pointwise
 import Mathlib.Data.Real.Sign