Merge pull request #134 from Ruben-VandeVelde/bump

Bump mathlib

Author: kbuzzard

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 α β σ₂ τ₂ :=

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 τ α))) =

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)

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)

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,