Bump mathlib

YaelDillies · Dec 29, 2024 · 30ad8bf · 30ad8bf
1 parent 11de551
commit 30ad8bf
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 23 deletions.
diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
@@ -36,7 +36,6 @@ import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
 import LeanCamCombi.Mathlib.Algebra.Order.Monoid.Unbundled.Pow
-import LeanCamCombi.Mathlib.Algebra.Polynomial.CoeffMem
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.Algebra.Ring.Hom.Defs
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic

diff --git a/LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean b/LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean
@@ -6,7 +6,6 @@ import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
 import LeanCamCombi.Mathlib.Algebra.Order.Monoid.Unbundled.Pow
-import LeanCamCombi.Mathlib.Algebra.Polynomial.CoeffMem
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
@@ -375,7 +374,7 @@ lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus :
     obtain ⟨S, hS, hS'⟩ := H f
     refine ⟨S, Eq.trans ?_ hS, ?_⟩
     · rw [← zeroLocus_span (Set.range _), ← zeroLocus_span (Set.range _),
-        idealSpan_range_update_divByMonic hne hi]
+        idealSpan_range_update_divByMonic hne _ hi]
     · intro C hC
       let c' : InductionObj _ _ := ⟨Function.update c.val j (c.val j %ₘ c.val i)⟩
       have deg_bound₁ : c'.degBound ≤ c.degBound := by

diff --git a/LeanCamCombi/Mathlib/Algebra/Polynomial/CoeffMem.lean b/LeanCamCombi/Mathlib/Algebra/Polynomial/CoeffMem.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "68fbd252aa5d0168c5f582c0f66b3005dba683e1",
+   "rev": "3f703ecb9714a08b92a17f9c3c19ffc32343fede",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,