From 5f0dceeefa6b9af809616a83a9bff2eff6643fe8 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 18 Sep 2024 20:19:21 +0200 Subject: [PATCH] Bump mathlib --- FLT/ForMathlib/MiscLemmas.lean | 24 ----------------------- FLT/MathlibExperiments/Frobenius.lean | 2 +- FLT/MathlibExperiments/Frobenius2.lean | 2 +- FLT/MathlibExperiments/FrobeniusRiou.lean | 4 ++-- lake-manifest.json | 12 ++++++------ 5 files changed, 10 insertions(+), 34 deletions(-) diff --git a/FLT/ForMathlib/MiscLemmas.lean b/FLT/ForMathlib/MiscLemmas.lean index be30592..d30e655 100644 --- a/FLT/ForMathlib/MiscLemmas.lean +++ b/FLT/ForMathlib/MiscLemmas.lean @@ -60,30 +60,6 @@ theorem coinduced_prod_eq_prod_coinduced {X Y S T : Type*} [AddCommGroup X] [Add end elsewhere -section missing_API - -variable {R : Type*} [Semiring R] {P : Type*} [AddCommMonoid P] [Module R P] - -namespace Module - --- the below is all done for rings but it should be semirings -/-- Free modules are projective. -/ -theorem Projective.of_basis' {ι : Type*} (b : Basis ι R P) : Projective R P := by - -- need P →ₗ (P →₀ R) for definition of projective. - -- get it from `ι → (P →₀ R)` coming from `b`. - use b.constr ℕ fun i => Finsupp.single (b i) (1 : R) - intro m - simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single, - map_finsupp_sum] - exact b.linearCombination_repr m - -instance (priority := 100) Projective.of_free' [Module.Free R P] : Module.Projective R P := - .of_basis' <| Module.Free.chooseBasis R P - -end Module - -end missing_API - theorem TopologicalSpace.prod_mono {α β : Type*} {σ₁ σ₂ : TopologicalSpace α} {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) : @instTopologicalSpaceProd α β σ₁ τ₁ ≤ @instTopologicalSpaceProd α β σ₂ τ₂ := diff --git a/FLT/MathlibExperiments/Frobenius.lean b/FLT/MathlibExperiments/Frobenius.lean index b1adeba..0e8aab7 100644 --- a/FLT/MathlibExperiments/Frobenius.lean +++ b/FLT/MathlibExperiments/Frobenius.lean @@ -488,7 +488,7 @@ theorem gal_smul_F_eq (σ : L ≃ₐ[K] L) : ∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B σ (galRestrict A K L B τ α))):= by - simp [Finset.smul_prod, smul_sub, smul_X, smul_C, AlgEquiv.smul_def] + simp [Finset.smul_prod', smul_sub, smul_X, smul_C, AlgEquiv.smul_def] /-- use `Finset.prod_bij` to show `(galRestrict A K L B σ • (∏ τ : L ≃ₐ[K] L, (X - C (galRestrict A K L B τ α))) = diff --git a/FLT/MathlibExperiments/Frobenius2.lean b/FLT/MathlibExperiments/Frobenius2.lean index b4e6c53..580e0dd 100644 --- a/FLT/MathlibExperiments/Frobenius2.lean +++ b/FLT/MathlibExperiments/Frobenius2.lean @@ -167,7 +167,7 @@ variable {A Q} in open Finset in lemma F.smul_eq_self (σ : B ≃ₐ[A] B) : σ • (F A Q) = F A Q := calc σ • F A Q = σ • ∏ τ : B ≃ₐ[A] B, (X - C (τ • (y A Q))) := by rw [F_spec] - _ = ∏ τ : B ≃ₐ[A] B, σ • (X - C (τ • (y A Q))) := smul_prod + _ = ∏ τ : B ≃ₐ[A] B, σ • (X - C (τ • (y A Q))) := smul_prod' _ = ∏ τ : B ≃ₐ[A] B, (X - C ((σ * τ) • (y A Q))) := by simp [smul_sub] _ = ∏ τ' : B ≃ₐ[A] B, (X - C (τ' • (y A Q))) := Fintype.prod_bijective (fun τ ↦ σ * τ) (Group.mulLeft_bijective σ) _ _ (fun _ ↦ rfl) diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean index 13e94d5..08ec72f 100644 --- a/FLT/MathlibExperiments/FrobeniusRiou.lean +++ b/FLT/MathlibExperiments/FrobeniusRiou.lean @@ -66,7 +66,7 @@ variable (P Q : Ideal B) [P.IsPrime] [Q.IsPrime] open scoped Pointwise private theorem norm_fixed (b : B) (g : G) : g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, σ • b := calc - g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := smul_finprod _ + g • (∏ᶠ σ : G, σ • b) = ∏ᶠ σ : G, g • (σ • b) := smul_finprod' _ _ = ∏ᶠ σ : G, σ • b := finprod_eq_of_bijective (g • ·) (MulAction.bijective g) fun x ↦ smul_smul g x b @@ -243,7 +243,7 @@ private theorem F_spec (b : B) : F G b = ∏ᶠ τ : G, (X - C (τ • b)) := rf private theorem F_smul_eq_self (σ : G) (b : B) : σ • (F G b) = F G b := calc σ • F G b = σ • ∏ᶠ τ : G, (X - C (τ • b)) := by rw [F_spec] - _ = ∏ᶠ τ : G, σ • (X - C (τ • b)) := smul_finprod _ + _ = ∏ᶠ τ : G, σ • (X - C (τ • b)) := smul_finprod' _ _ = ∏ᶠ τ : G, (X - C ((σ * τ) • b)) := by simp [smul_sub, smul_smul] _ = ∏ᶠ τ' : G, (X - C (τ' • b)) := finprod_eq_of_bijective (fun τ ↦ σ * τ) (Group.mulLeft_bijective σ) (fun _ ↦ rfl) diff --git a/lake-manifest.json b/lake-manifest.json index cfb87da..9d4632b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85", + "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7", + "rev": "2c39748d927749624f480b641f1d2d77b8632b92", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -61,11 +61,11 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git", + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, - "scope": "", - "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1", + "scope": "leanprover-community", + "rev": "3e9460c40e09457b2fd079ef55316535536425fc", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7eb3f52a4fc12036cb1c4a953dd0f497b57a2434", + "rev": "95af9be74f8b9d98505d9900fe8f563a89e5e667", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,