From cf2437c1adfce708a278330c9f35799461ec6acf Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 19 Feb 2025 13:01:52 +0100 Subject: [PATCH] chore: bump mathlib (#350) --- FLT/AutomorphicRepresentation/Example.lean | 4 ++-- FLT/DivisionAlgebra/Finiteness.lean | 2 +- FLT/GlobalLanglandsConjectures/GLnDefs.lean | 2 +- FLT/HaarMeasure/DistribHaarChar/Basic.lean | 2 +- FLT/HaarMeasure/DomMulActMeasure.lean | 2 +- .../NumberTheory/Padics/PadicIntegers.lean | 2 +- .../Topology/Algebra/ContinuousMonoidHom.lean | 2 +- .../Algebra/Module/ModuleTopology.lean | 22 +++++++++---------- .../Topology/Algebra/Module/Quotient.lean | 2 +- FLT/Mathlib/Topology/Algebra/UniformRing.lean | 8 +++---- lake-manifest.json | 4 ++-- 11 files changed, 26 insertions(+), 26 deletions(-) diff --git a/FLT/AutomorphicRepresentation/Example.lean b/FLT/AutomorphicRepresentation/Example.lean index 6c77d2c1..5789ac13 100644 --- a/FLT/AutomorphicRepresentation/Example.lean +++ b/FLT/AutomorphicRepresentation/Example.lean @@ -546,7 +546,7 @@ instance : Zero 𝓞 := ⟨zero⟩ @[simp] lemma zero_im_oi : im_oi (0 : 𝓞) = 0 := rfl lemma toQuaternion_zero : toQuaternion 0 = 0 := by - ext <;> simp [toQuaternion] + ext <;> (simp [toQuaternion]; aesop) @[simp] lemma toQuaternion_eq_zero_iff {z} : toQuaternion z = 0 ↔ z = 0 := @@ -568,7 +568,7 @@ instance : One 𝓞 := ⟨one⟩ @[simp] lemma one_im_oi : im_oi (1 : 𝓞) = 0 := rfl lemma toQuaternion_one : toQuaternion 1 = 1 := by - ext <;> simp [toQuaternion] + ext <;> (simp [toQuaternion]; aesop) /-! ## Neg (-) -/ diff --git a/FLT/DivisionAlgebra/Finiteness.lean b/FLT/DivisionAlgebra/Finiteness.lean index 7c6d1497..18a52670 100644 --- a/FLT/DivisionAlgebra/Finiteness.lean +++ b/FLT/DivisionAlgebra/Finiteness.lean @@ -45,7 +45,7 @@ local instance : IsModuleTopology (FiniteAdeleRing (𝓞 K) K) (D ⊗[K] (Finite variable [FiniteDimensional K D] -instance : TopologicalRing (D ⊗[K] (FiniteAdeleRing (𝓞 K) K)) := +instance : IsTopologicalRing (D ⊗[K] (FiniteAdeleRing (𝓞 K) K)) := IsModuleTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 K) K) _ variable [Algebra.IsCentral K D] diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean index 5b6cef0d..ed116a2e 100644 --- a/FLT/GlobalLanglandsConjectures/GLnDefs.lean +++ b/FLT/GlobalLanglandsConjectures/GLnDefs.lean @@ -91,7 +91,7 @@ lemma FiniteAdeleRing.clear_denominator (a : FiniteAdeleRing R K) : instance : TopologicalSpace (FiniteAdeleRing ℤ ℚ) := sorry -instance instTopologicalRingFiniteAdeleRing : TopologicalRing (FiniteAdeleRing ℤ ℚ) := sorry +instance instTopologicalRingFiniteAdeleRing : IsTopologicalRing (FiniteAdeleRing ℤ ℚ) := sorry end PR13703 diff --git a/FLT/HaarMeasure/DistribHaarChar/Basic.lean b/FLT/HaarMeasure/DistribHaarChar/Basic.lean index 0081958d..4f0d5a14 100644 --- a/FLT/HaarMeasure/DistribHaarChar/Basic.lean +++ b/FLT/HaarMeasure/DistribHaarChar/Basic.lean @@ -30,7 +30,7 @@ variable {G A : Type*} [Group G] [AddCommGroup A] [DistribMulAction G A] [MeasurableSMul G A] -- only need `MeasurableConstSMul` but we don't have this class. variable {μ ν : Measure A} {g : G} -variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCompactSpace A] +variable [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A] [LocallyCompactSpace A] [ContinuousConstSMul G A] [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] variable (μ A) in diff --git a/FLT/HaarMeasure/DomMulActMeasure.lean b/FLT/HaarMeasure/DomMulActMeasure.lean index 61c0ee1a..b0e824bc 100644 --- a/FLT/HaarMeasure/DomMulActMeasure.lean +++ b/FLT/HaarMeasure/DomMulActMeasure.lean @@ -26,7 +26,7 @@ lemma integral_domSMul {α} [NormedAddCommGroup α] [NormedSpace ℝ α] (g : G ∫ x, f x ∂g • μ = ∫ x, f ((DomMulAct.mk.symm g)⁻¹ • x) ∂μ := integral_map_equiv (MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)) f -variable [TopologicalSpace A] [BorelSpace A] [TopologicalAddGroup A] [LocallyCompactSpace A] +variable [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A] [LocallyCompactSpace A] [ContinuousConstSMul G A] [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] instance : SMulCommClass ℝ≥0 Gᵈᵐᵃ (Measure A) where diff --git a/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean index 56135d65..c295fe95 100644 --- a/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/FLT/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -71,7 +71,7 @@ lemma smul_submodule_finiteRelIndex (hx : x ≠ 0) (s : Submodule ℤ_[p] ℚ_[p -- Yaël: Do we really want this as a coercion? noncomputable instance : Coe ℤ_[p]⁰ ℚ_[p]ˣ where - coe x := .mk0 x.1 <| map_ne_zero_of_mem_nonZeroDivisors (M := ℤ_[p]) Coe.ringHom coe_injective x.2 + coe x := .mk0 x.1 <| map_ne_zero_of_mem_nonZeroDivisors (M₀ := ℤ_[p]) Coe.ringHom coe_injective x.2 /-- Non-zero p-adic integers generate non-zero p-adic numbers as a group. -/ lemma closure_nonZeroDivisors_padicInt : diff --git a/FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean index 15288c2d..50b608d3 100644 --- a/FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean +++ b/FLT/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean @@ -12,7 +12,7 @@ def ContinuousAddEquiv.toIntContinuousLinearEquiv {M M₂ : Type*} [AddCommGroup def ContinuousAddEquiv.quotientPi {ι : Type*} {G : ι → Type*} [(i : ι) → AddCommGroup (G i)] [(i : ι) → TopologicalSpace (G i)] - [(i : ι) → TopologicalAddGroup (G i)] + [(i : ι) → IsTopologicalAddGroup (G i)] [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] : ((i : ι) → G i) ⧸ AddSubgroup.pi (_root_.Set.univ) p ≃ₜ+ ((i : ι) → G i ⧸ p i) := (Submodule.quotientPiContinuousLinearEquiv diff --git a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean index c324f56e..347c72c5 100644 --- a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean +++ b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean @@ -49,7 +49,7 @@ theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι] haveI : ContinuousAdd C := toContinuousAdd R C exact continuous_finsum (fun i ↦ by fun_prop) (locallyFinite_of_finite _) -theorem Module.continuous_bilinear_of_finite_free [TopologicalSemiring R] [Module.Finite R A] +theorem Module.continuous_bilinear_of_finite_free [IsTopologicalSemiring R] [Module.Finite R A] [Module.Free R A] (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) := by let ι := Module.Free.ChooseBasisIndex R A @@ -72,7 +72,7 @@ end semiring_bilinear section ring_bilinear -variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [TopologicalRing R] +variable {R : Type*} [τR : TopologicalSpace R] [CommRing R] [IsTopologicalRing R] variable {A : Type*} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] variable {B : Type*} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B] @@ -107,7 +107,7 @@ section semiring_algebra open scoped TensorProduct -- these shouldn't be rings, they should be semirings -variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R] +variable (R) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D] variable [TopologicalSpace D] [IsModuleTopology R D] @@ -115,12 +115,12 @@ open scoped TensorProduct @[continuity, fun_prop] theorem continuous_mul' - (R : Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R] + (R : Type*) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] [Module.Free R D] [TopologicalSpace D] [IsModuleTopology R D] : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := Module.continuous_bilinear_of_finite (LinearMap.mul R D) -def topologicalSemiring : TopologicalSemiring D where +def topologicalSemiring : IsTopologicalSemiring D where continuous_add := (toContinuousAdd R D).1 continuous_mul := continuous_mul' R D @@ -130,7 +130,7 @@ section ring_algebra -- confusion about whether these are rings or semirings should ideally be resolved -- Is it: for D finite free R can be a semiring but for D finite it has to be a ring? -variable (R) [CommRing R] [TopologicalSpace R] [TopologicalRing R] +variable (R) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] variable (D : Type*) [Ring D] [Algebra R D] [Module.Finite R D] variable [TopologicalSpace D] [IsModuleTopology R D] @@ -143,7 +143,7 @@ theorem continuous_mul : Continuous (fun ab ↦ ab.1 * ab.2 : D × D → D) := b haveI : IsModuleTopology R (D ⊗[R] D) := { eq_moduleTopology' := rfl } convert Module.continuous_bilinear_of_finite <| (LinearMap.mul R D : D →ₗ[R] D →ₗ[R] D) -def Module.topologicalRing : TopologicalRing D where +def Module.topologicalRing : IsTopologicalRing D where continuous_add := (toContinuousAdd R D).1 continuous_mul := continuous_mul R D continuous_neg := continuous_neg R D @@ -155,8 +155,8 @@ end ring_algebra section trans variable (R S M : Type*) - [CommRing R] [TopologicalSpace R] [TopologicalRing R] - [CommRing S] [TopologicalSpace S] [TopologicalRing S] + [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] + [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [Algebra R S] [Module.Finite R S] [IsModuleTopology R S] [AddCommGroup M] [Module R M] @@ -193,8 +193,8 @@ end trans section opensubring variable (R S : Type*) - [CommRing R] [TopologicalSpace R] [TopologicalRing R] - [CommRing S] [TopologicalSpace S] [TopologicalRing S] + [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] + [CommRing S] [TopologicalSpace S] [IsTopologicalRing S] [Algebra R S] example (hcont : Continuous (algebraMap R S)) diff --git a/FLT/Mathlib/Topology/Algebra/Module/Quotient.lean b/FLT/Mathlib/Topology/Algebra/Module/Quotient.lean index 3290cf50..59e41aa6 100644 --- a/FLT/Mathlib/Topology/Algebra/Module/Quotient.lean +++ b/FLT/Mathlib/Topology/Algebra/Module/Quotient.lean @@ -17,7 +17,7 @@ def Submodule.Quotient.continuousLinearEquiv {R : Type*} [Ring R] (G H : Type*) def Submodule.quotientPiContinuousLinearEquiv {R ι : Type*} [CommRing R] {G : ι → Type*} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] [(i : ι) → TopologicalSpace (G i)] - [(i : ι) → TopologicalAddGroup (G i)] [Fintype ι] [DecidableEq ι] + [(i : ι) → IsTopologicalAddGroup (G i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (G i)) : (((i : ι) → G i) ⧸ Submodule.pi Set.univ p) ≃L[R] ((i : ι) → G i ⧸ p i) where toLinearEquiv := Submodule.quotientPi p diff --git a/FLT/Mathlib/Topology/Algebra/UniformRing.lean b/FLT/Mathlib/Topology/Algebra/UniformRing.lean index 8b276824..d564dd9d 100644 --- a/FLT/Mathlib/Topology/Algebra/UniformRing.lean +++ b/FLT/Mathlib/Topology/Algebra/UniformRing.lean @@ -7,8 +7,8 @@ import FLT.Mathlib.Algebra.Algebra.Hom namespace UniformSpace.Completion -variable {α : Type*} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] - {β : Type*} [UniformSpace β] [Ring β] [UniformAddGroup β] [TopologicalRing β] +variable {α : Type*} [Ring α] [UniformSpace α] [IsTopologicalRing α] [UniformAddGroup α] + {β : Type*} [UniformSpace β] [Ring β] [UniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous f) theorem mapRingHom_apply {x : UniformSpace.Completion α} : @@ -21,8 +21,8 @@ theorem mapRingHom_coe (hf : UniformContinuous f) (a : α) : rw [mapRingHom_apply, map_coe hf] noncomputable def mapSemialgHom {α : Type*} [CommRing α] [UniformSpace α] - [TopologicalRing α] [UniformAddGroup α] {β : Type*} [UniformSpace β] [CommRing β] - [UniformAddGroup β] [TopologicalRing β] (f : α →+* β) (hf : Continuous f) : + [IsTopologicalRing α] [UniformAddGroup α] {β : Type*} [UniformSpace β] [CommRing β] + [UniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous f) : Completion α →ₛₐ[f] Completion β where __ := UniformSpace.Completion.mapRingHom f hf map_smul' m x := by diff --git a/lake-manifest.json b/lake-manifest.json index 5a28dcab..5bcb477b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "6b28ba204395930a138b9e9151ba8c473ac7d811", + "rev": "2836c275479466837c2593377bb54ae9fafc41d2", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b18855cb0f9a19bd4d7e21f3e5525272e377f431", + "rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",