Bump mathlib

YaelDillies · Aug 29, 2024 · c882698 · c882698
1 parent 1650046
commit c882698
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 9 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -9,7 +9,6 @@ import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
-import LeanAPAP.Mathlib.Data.NNReal.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs

diff --git a/LeanAPAP/Mathlib/Data/NNReal/Basic.lean b/LeanAPAP/Mathlib/Data/NNReal/Basic.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6ce4187086ef93261927bbc72d061888099b30fc",
+   "rev": "0844193bcedb553ac72342e6ac8b6ae9a5287a14",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,