Bump mathlib

teorth · Oct 3, 2024 · 1aca48a · 1aca48a
1 parent ebd4d5b
commit 1aca48a
Show file tree

Hide file tree

Showing 9 changed files with 14 additions and 19 deletions.
diff --git a/PFR/ApproxHomPFR.lean b/PFR/ApproxHomPFR.lean
@@ -2,6 +2,7 @@ import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Analysis.Normed.Lp.PiLp
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Extras.BSG
+import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.HomPFR
 
 /-!

diff --git a/PFR/ForMathlib/Elementary.lean b/PFR/ForMathlib/Elementary.lean
@@ -1,5 +1,5 @@
+import Mathlib.Algebra.Module.ZMod
 import Mathlib.Data.Finsupp.Fintype
-import Mathlib.Data.ZMod.Module
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.GroupTheory.Sylow
 

diff --git a/PFR/ForMathlib/Entropy/Kernel/Basic.lean b/PFR/ForMathlib/Entropy/Kernel/Basic.lean
@@ -1,6 +1,7 @@
 import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import PFR.ForMathlib.Entropy.Measure
 import PFR.Mathlib.MeasureTheory.Integral.Bochner
+import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
 import PFR.Mathlib.MeasureTheory.MeasurableSpace.Defs
 import PFR.Mathlib.Probability.Kernel.Disintegration
 

diff --git a/PFR/ForMathlib/Entropy/Measure.lean b/PFR/ForMathlib/Entropy/Measure.lean
@@ -1,10 +1,9 @@
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
+import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
 import PFR.ForMathlib.FiniteRange
 import PFR.ForMathlib.MeasureReal
 import PFR.Mathlib.MeasureTheory.Constructions.Prod.Basic
-import PFR.Mathlib.MeasureTheory.Integral.Bochner
-import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
 import PFR.Tactic.Finiteness
 
 /-!

diff --git a/PFR/ForMathlib/Entropy/RuzsaSetDist.lean b/PFR/ForMathlib/Entropy/RuzsaSetDist.lean
@@ -5,7 +5,6 @@ import PFR.ForMathlib.Entropy.Basic
 import PFR.ForMathlib.Entropy.RuzsaDist
 import PFR.ForMathlib.MeasureReal
 import PFR.ForMathlib.Uniform
-import PFR.Mathlib.Data.Set.Pointwise.Finite
 
 section UniformMeasure
 

diff --git a/PFR/Main.lean b/PFR/Main.lean
@@ -3,7 +3,6 @@ import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.OrderOfElement
 import PFR.EntropyPFR
-import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.Tactic.RPowSimp
 import PFR.TauFunctional
 

diff --git a/PFR/Mathlib/Data/Set/Pointwise/Finite.lean b/PFR/Mathlib/Data/Set/Pointwise/Finite.lean
@@ -4,10 +4,6 @@ import PFR.Mathlib.Data.Set.Function
 open Function
 open scoped Pointwise
 
-@[to_additive]
-lemma Set.Finite.div {α : Type*} [Div α] {A B : Set α} (hA : A.Finite) (hB : B.Finite) :
-    Set.Finite (A / B) := Set.Finite.image2 _ hA hB
-
 namespace Set
 variable {α β γ : Type*} {f g : α → β} {x : α × β}
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
+   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0",
+   "rev": "bb7a404341c1b8f113a011a0a60b367b7d2649ff",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fb91e3382a706b33843488a2988e79a44f56ba2f",
+   "rev": "6b9c902f71d714a7d4cf219b3a400f14a7e108e4",
    "name": "LeanAPAP",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
+   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
+   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
+   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.12.0