Bump 2024 12 25 (#293)

* Bump mathlib * lean4#6325 still not fixed --------- Co-authored-by: Yaël Dillies <[email protected]>
ImperialCollegeLondon · Dec 25, 2024 · 68ec7c4 · 68ec7c4
1 parent 7a9b622
commit 68ec7c4
Show file tree

Hide file tree

Showing 7 changed files with 17 additions and 64 deletions.
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -3,48 +3,50 @@ import FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
 import FLT.AutomorphicRepresentation.Example
 import FLT.Basic.Reductions
 import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
+import FLT.Deformations.RepresentationTheory.Irreducible
+import FLT.Deformations.RepresentationTheory.Subrepresentation
 import FLT.DivisionAlgebra.Finiteness
 import FLT.EllipticCurve.Torsion
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.flatness
 import FLT.HaarMeasure.DistribHaarChar.Basic
 import FLT.HaarMeasure.DistribHaarChar.Padic
 import FLT.HaarMeasure.DistribHaarChar.RealComplex
 import FLT.HaarMeasure.DomMulActMeasure
 import FLT.HaarMeasure.MeasurableSpacePadics
 import FLT.Hard.Results
-import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
 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.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.MathlibExperiments.Coalgebra.Monoid
-import FLT.MathlibExperiments.Coalgebra.Sweedler
-import FLT.MathlibExperiments.Coalgebra.TensorProduct
-import FLT.MathlibExperiments.HopfAlgebra.Basic
-import FLT.MathlibExperiments.IsCentralSimple
-import FLT.MathlibExperiments.IsFrobenius
 import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 import FLT.Mathlib.LinearAlgebra.Determinant
+import FLT.Mathlib.LinearAlgebra.Span.Defs
 import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.NumberField.Completion
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.RepresentationTheory.Basic
 import FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv
-import FLT.Mathlib.Topology.Algebra.Module.Basic
+import FLT.Mathlib.Topology.Algebra.Module.Equiv
 import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Topology.Algebra.Monoid
 import FLT.Mathlib.Topology.Constructions
 import FLT.Mathlib.Topology.Homeomorph
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.HopfAlgebra.Basic
+import FLT.MathlibExperiments.IsCentralSimple
+import FLT.MathlibExperiments.IsFrobenius
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
 import FLT.NumberField.IsTotallyReal

diff --git a/FLT/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/FLT/Mathlib/Algebra/Group/Subgroup/Pointwise.lean
diff --git a/FLT/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean b/FLT/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
diff --git a/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean
@@ -1,12 +1,10 @@
 import Mathlib.Algebra.CharZero.Infinite
 import Mathlib.NumberTheory.Padics.PadicIntegers
-import FLT.Mathlib.Algebra.Group.Subgroup.Pointwise
 import FLT.Mathlib.GroupTheory.Index
 
 /-!
 # TODO
 
-* Make `PadicInt.valuation` `ℕ`-valued
 * Rename `Coe.ringHom` to `coeRingHom`
 * Protect `PadicInt.norm_mul`, `PadicInt.norm_units`, `PadicInt.norm_pow`
 -/
@@ -39,9 +37,6 @@ protected lemma nnnorm_pow (x : ℤ_[p]) (n : ℕ) : ‖x ^ n‖₊ = ‖x‖₊
 
 @[simp] protected lemma nnnorm_units (u : ℤ_[p]ˣ) : ‖(u : ℤ_[p])‖₊ = 1 := by simp [nnnorm, NNReal]
 
--- TODO: Replace `valuation`
-noncomputable def valuation' (a : ℤ_[p]) : ℕ := a.valuation.toNat
-
 lemma exists_unit_mul_p_pow_eq (hx : x ≠ 0) : ∃ (u : ℤ_[p]ˣ) (n : ℕ), (u : ℤ_[p]) * p ^ n = x :=
   ⟨_, _, (unitCoeff_spec hx).symm⟩
 

diff --git a/...athlib/Topology/Algebra/Module/Basic.lean → ...athlib/Topology/Algebra/Module/Equiv.lean b/...athlib/Topology/Algebra/Module/Basic.lean → ...athlib/Topology/Algebra/Module/Equiv.lean
@@ -1,4 +1,4 @@
-import Mathlib.Topology.Algebra.Module.Basic
+import Mathlib.Topology.Algebra.Module.Equiv
 import FLT.Mathlib.Algebra.Module.Equiv.Defs
 import FLT.Mathlib.Topology.Homeomorph
 
@@ -13,7 +13,6 @@ def ContinuousLinearEquiv.piCongrLeft (R : Type*) [Semiring R] {ι ι' : Type*}
   __ := Homeomorph.piCongrLeft e
   __ := LinearEquiv.piCongrLeft R φ e
 
-
 section Pi
 
 /-- The space of functions from `S ⊕ T` into a family of topological modules

diff --git a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
@@ -2,7 +2,7 @@ import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
-import FLT.Mathlib.Topology.Algebra.Module.Basic
+import FLT.Mathlib.Topology.Algebra.Module.Equiv
 import FLT.Mathlib.Topology.Algebra.Monoid
 
 /-!
@@ -71,29 +71,6 @@ namespace IsModuleTopology
 
 open ModuleTopology
 
--- this section PRed in mathlib #20012
-section function
-
-variable {R : Type*} [τR : TopologicalSpace R] [Semiring R]
-variable {A : Type*} [AddCommMonoid A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A]
-variable {B : Type*} [AddCommMonoid B] [Module R B] [aB : TopologicalSpace B]
-    [ContinuousAdd B] [ContinuousSMul R B]
-
-variable (R) in
-theorem continuousNeg (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C]
-    [IsModuleTopology R C] : ContinuousNeg C where
-  continuous_neg :=
-    haveI : ContinuousAdd C := IsModuleTopology.toContinuousAdd R C
-    continuous_of_linearMap (LinearEquiv.neg R).toLinearMap
-
-variable (R) in
-theorem topologicalAddGroup (C : Type*) [AddCommGroup C] [Module R C] [TopologicalSpace C]
-    [IsModuleTopology R C] : TopologicalAddGroup C where
-      continuous_add := (IsModuleTopology.toContinuousAdd R C).1
-      continuous_neg := (continuousNeg R C).1
-
-end function
-
 -- this section PRed in mathlib #20012
 section surjection
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9c324ade60adf9b37f4f7b49776bd2bb3a82d5e9",
+   "rev": "fd52917a1ac853bcb73cd089ce43e6a4257c98e0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "49ac6bf04dc187ffc0a056421c603fcefce6991a",
+   "rev": "9c1fb88357e7f6da8f332342f9a67e3816c4fa55",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
+   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",