bump

Author: riccardobrasca

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -274,7 +274,7 @@ lemma separable_poly (I : Ideal (𝓞 K)) [I.IsMaximal] :
 lemma polyRoot_spec {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ p = algebraMap K L u) (i) :
     α = (ζ ^ i)⁻¹ • (1 - (ζ - 1) • (polyRoot hp hζ u hcong α e i : L)) := by
-  apply smul_right_injective (M := L) (c := ζ ^ i) (pow_ne_zero _ <| hζ.ne_zero
+  apply smul_right_injective (M := L) (r := ζ ^ i) (pow_ne_zero _ <| hζ.ne_zero
     (NeZero.pos p).ne.symm)
   simp only [polyRoot, map_sub, map_one, NumberField.RingOfIntegers.map_mk,
     Algebra.smul_def (ζ - 1), ← mul_div_assoc,

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "05bb84181739ecc0897184a3e2906241267bcdfd",
+   "rev": "cc1a61983e46cf9185c198e96f15542336dc2413",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "15f6691e7a582dab598395c89b04c451f81b8049",
+   "rev": "53b324fd0c646e0b2d68cbaae666d40a02d20517",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bc7b7f567dacc39ae904b6f12f6aa7f90e48e45f",
+   "rev": "5ba0380f2fb45c69448d80429ef6c22bf5973cfa",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",