feat: port Data.Real.ENNReal (#2388)

I did some fixes/refactors while working on this PR. I'm going to move them to new PRs soon.
leanprover-community · Feb 27, 2023 · 1979f8d · 1979f8d
1 parent 3735887
commit 1979f8d
Show file tree

Hide file tree

Showing 2 changed files with 2,482 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -647,6 +647,7 @@ import Mathlib.Data.Rat.Sqrt
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.CauSeq
 import Mathlib.Data.Real.CauSeqCompletion
+import Mathlib.Data.Real.ENNReal
 import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pointwise
 import Mathlib.Data.Real.Sign