bump mathlib (#290)

ImperialCollegeLondon · Dec 19, 2024 · cc6ed6e · cc6ed6e
1 parent b5e3527
commit cc6ed6e
Show file tree

Hide file tree

Showing 7 changed files with 3 additions and 77 deletions.
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -27,9 +27,6 @@ import FLT.Mathlib.Algebra.Module.Equiv.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
-import FLT.Mathlib.Analysis.Complex.Basic
-import FLT.Mathlib.Data.Complex.Basic
-import FLT.Mathlib.Data.ENNReal.Inv
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct

diff --git a/FLT/HaarMeasure/DistribHaarChar/Basic.lean b/FLT/HaarMeasure/DistribHaarChar/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Yaël Dillies, Javier López-Contreras
 -/
 import FLT.HaarMeasure.DomMulActMeasure
-import FLT.Mathlib.Data.ENNReal.Inv
 
 /-!
 # The distributive character of Haar measures

diff --git a/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean b/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean
@@ -8,8 +8,6 @@ import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import Mathlib.RingTheory.Complex
 import Mathlib.RingTheory.Norm.Transitivity
 import FLT.HaarMeasure.DistribHaarChar.Basic
-import FLT.Mathlib.Analysis.Complex.Basic
-import FLT.Mathlib.Data.Complex.Basic
 import FLT.Mathlib.LinearAlgebra.Determinant
 
 /-!

diff --git a/FLT/Mathlib/Analysis/Complex/Basic.lean b/FLT/Mathlib/Analysis/Complex/Basic.lean
diff --git a/FLT/Mathlib/Data/Complex/Basic.lean b/FLT/Mathlib/Data/Complex/Basic.lean
diff --git a/FLT/Mathlib/Data/ENNReal/Inv.lean b/FLT/Mathlib/Data/ENNReal/Inv.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e47321100938852afffd41c3c882ba637662d354",
+   "rev": "9c324ade60adf9b37f4f7b49776bd2bb3a82d5e9",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "495ec69bfbbe8fe20099db76e889e39b676ba43f",
+   "rev": "49ac6bf04dc187ffc0a056421c603fcefce6991a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
+   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",