chore: bump mathlib

ImperialCollegeLondon · Dec 17, 2024 · b6ba352 · b6ba352
1 parent 0986ffc
commit b6ba352
Show file tree

Hide file tree

Showing 6 changed files with 4 additions and 32 deletions.
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -23,7 +23,6 @@ import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
 import FLT.Mathlib.Algebra.BigOperators.Finprod
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
 import FLT.Mathlib.Algebra.Group.Subgroup.Pointwise
-import FLT.Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import FLT.Mathlib.Algebra.Module.Equiv.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
@@ -46,7 +45,6 @@ import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.NumberField.Completion
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
-import FLT.Mathlib.RingTheory.Norm.Defs
 import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
 import FLT.Mathlib.Topology.Algebra.Module.Basic
 import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology

diff --git a/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean b/FLT/HaarMeasure/DistribHaarChar/RealComplex.lean
@@ -6,11 +6,11 @@ Authors: Yaël Dillies, Javier López-Contreras
 import Mathlib.Analysis.Complex.ReImTopology
 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
-import FLT.Mathlib.RingTheory.Norm.Defs
 
 /-!
 # The distributive Haar characters of `ℝ` and `ℂ`

diff --git a/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean b/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
diff --git a/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
@@ -1,7 +1,6 @@
 import Mathlib.Algebra.CharZero.Infinite
 import Mathlib.NumberTheory.Padics.PadicIntegers
 import FLT.Mathlib.Algebra.Group.Subgroup.Pointwise
-import FLT.Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import FLT.Mathlib.GroupTheory.Index
 
 /-!

diff --git a/FLT/Mathlib/RingTheory/Norm/Defs.lean b/FLT/Mathlib/RingTheory/Norm/Defs.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "82c0223cfb0ba31bcf8bef02519adb92fecf4421",
+   "rev": "e47321100938852afffd41c3c882ba637662d354",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d70fcf43625e913424f156c19d1f378ad5117f02",
+   "rev": "495ec69bfbbe8fe20099db76e889e39b676ba43f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668",
+   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",