Bump mathlib

teorth · Oct 19, 2024 · ee35aa0 · ee35aa0
1 parent 9ac7f5b
commit ee35aa0
Show file tree

Hide file tree

Showing 10 changed files with 6 additions and 45 deletions.
diff --git a/PFR.lean b/PFR.lean
@@ -32,9 +32,6 @@ import PFR.ImprovedPFR
 import PFR.Kullback
 import PFR.Main
 import PFR.Mathlib.Algebra.Group.Pointwise.Set.Basic
-import PFR.Mathlib.Algebra.Module.Submodule.Ker
-import PFR.Mathlib.Algebra.Module.Submodule.Map
-import PFR.Mathlib.Algebra.Module.Submodule.Range
 import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
 import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.Mathlib.Data.Set.Pointwise.SMul

diff --git a/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean b/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean
@@ -1,4 +1,3 @@
-import PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
 import PFR.ForMathlib.Entropy.Kernel.Group
 
 /-!

diff --git a/PFR/ImprovedPFR.lean b/PFR/ImprovedPFR.lean
@@ -1028,7 +1028,7 @@ theorem PFR_conjecture_improv (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K
     refine ⟨H', c + u, ?_, IH'A, by rwa [add_assoc, HH'u]⟩
     calc
     (Nat.card (c + u) : ℝ)
-      ≤ Nat.card c * Nat.card u := mod_cast card_add_le
+      ≤ Nat.card c * Nat.card u := mod_cast natCard_add_le
     _ ≤ (K ^ 6 * Nat.card A ^ (1 / 2) * (Nat.card H ^ (-1 / 2)))
           * (Nat.card H / Nat.card H') := by
         gcongr

diff --git a/PFR/Mathlib/Algebra/Module/Submodule/Ker.lean b/PFR/Mathlib/Algebra/Module/Submodule/Ker.lean
diff --git a/PFR/Mathlib/Algebra/Module/Submodule/Map.lean b/PFR/Mathlib/Algebra/Module/Submodule/Map.lean
diff --git a/PFR/Mathlib/Algebra/Module/Submodule/Range.lean b/PFR/Mathlib/Algebra/Module/Submodule/Range.lean
diff --git a/PFR/Mathlib/LinearAlgebra/Basis/VectorSpace.lean b/PFR/Mathlib/LinearAlgebra/Basis/VectorSpace.lean
@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Module.Projective
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 
 namespace Submodule

diff --git a/PFR/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/PFR/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
diff --git a/PFR/WeakPFR.lean b/PFR/WeakPFR.lean
@@ -1,8 +1,5 @@
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
-import PFR.Mathlib.Algebra.Module.Submodule.Ker
-import PFR.Mathlib.Algebra.Module.Submodule.Map
-import PFR.Mathlib.Algebra.Module.Submodule.Range
 import PFR.Mathlib.Data.Set.Pointwise.SMul
 import PFR.ForMathlib.AffineSpaceDim
 import PFR.ForMathlib.Entropy.RuzsaSetDist

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c521f0185f4dd42b6aa4898010d5ba5357c57c9f",
+   "rev": "10130798199d306703dee5ab2567961444ebbd04",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3f297f53816d8a85d03f8c08b3a7d475dfa51a6b",
+   "rev": "66f63643834286e06540e60e459b22c7bbd25475",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1f236c616968ac588983fddd0b4ed2cf58483670",
+   "rev": "ece13c901dde033807bd3c72c40c9ae48f060f7b",
    "name": "LeanAPAP",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,