Bump mathlib

Author: YaelDillies

PFR.lean

@@ -22,7 +22,6 @@ import PFR.ForMathlib.FiniteMeasureProd
 import PFR.ForMathlib.FiniteRange.ConditionalProbability
 import PFR.ForMathlib.FiniteRange.Defs
 import PFR.ForMathlib.FiniteRange.IdentDistrib
-import PFR.ForMathlib.GroupQuot
 import PFR.ForMathlib.MeasureReal.Defs
 import PFR.ForMathlib.MeasureReal.Indep
 import PFR.ForMathlib.MeasureReal.UniformOn

PFR/ForMathlib/GroupQuot.lean

@@ -1,12 +1,12 @@
 import Mathlib.GroupTheory.Torsion
 import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
+import Mathlib.LinearAlgebra.FreeModule.ModN
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
 import PFR.Mathlib.Data.Set.Pointwise.SMul
 import PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 import PFR.ForMathlib.AffineSpaceDim
 import PFR.ForMathlib.Entropy.RuzsaSetDist
-import PFR.ForMathlib.GroupQuot
 import PFR.ImprovedPFR
 
 /-!

PFR/WeakPFR.lean

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0177f355e733fd7caebad72d1308219b302a8d1f",
+   "rev": "16f61b7761caa9784f17b1b22bfe989f4499afb4",
    "name": "LeanAPAP",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b1df36dae55e50867f35dabde48f516c0a07c12a",
+   "rev": "215e9c6293496e3cccee65b4f66ebdc22c8ad728",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9",
+   "rev": "35f683e2d8c1ff031e52e397efeb9bc0a74d83dd",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143",
+   "rev": "6635f4e1607ca8c70c5bec6bb288493b8f3e567b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",