Bump mathlib

YaelDillies · Nov 17, 2024 · 9c77372 · 9c77372
1 parent a59ff39
commit 9c77372
Show file tree

Hide file tree

Showing 6 changed files with 1 addition and 32 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -3,8 +3,6 @@ import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Order.LiminfLimsup
-import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Probability.UniformOn
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity

diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -1,6 +1,5 @@
 import Mathlib.Data.Fintype.Order
 import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 noncomputable section
 

diff --git a/LeanAPAP/Mathlib/Order/LiminfLimsup.lean b/LeanAPAP/Mathlib/Order/LiminfLimsup.lean
diff --git a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
diff --git a/LeanAPAP/Mathlib/Probability/UniformOn.lean b/LeanAPAP/Mathlib/Probability/UniformOn.lean
@@ -1,5 +1,4 @@
 import Mathlib.Probability.UniformOn
-import LeanAPAP.Mathlib.Probability.ConditionalProbability
 
 namespace ProbabilityTheory
 variable {Ω : Type*} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω}

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79635cf94d5bbd65851b5e47c0149c7e58f1b73a",
+   "rev": "59e75948eb18b0946b93c99d666844ca885675c6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,