bump

Author: riccardobrasca

FltRegular/NumberTheory/Hilbert92.lean

@@ -34,6 +34,7 @@ abbrev systemOfUnits.IsMaximal {p : ℕ} {G : Type*} [AddCommGroup G]
   Fintype (G ⧸ Submodule.span (CyclotomicIntegers p) (Set.range sys.units))
 
 set_option backward.isDefEq.respectTransparency false in
+@[reducible]
 noncomputable
 def systemOfUnits.isMaximal [Module.Finite ℤ G] (hf : finrank ℤ G = s * (p - 1))
   [Module A G] (sys : systemOfUnits (G := G) p s) : sys.IsMaximal := by

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "dc43f26dcfad8ba328108534fc4facdf77428a38",
+   "rev": "47562571f3b443f46bf708b71727c0e904f9d6cb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b93f2523263a6df8a8fbbe3dd28b7f028087480",
+   "rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ea1e51a85f6bd53b6a84239b00593eebd03d522b",
+   "rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "212dc300449e436298804f09b264f624667106f8",
+   "rev": "2e58165a9dcdca9837b666528f974299ee1a51cc",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.90",
+   "inputRev": "v0.0.92",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6f8999a4e31701d2c905262d3788a8c0d21b3f1f",
+   "rev": "c3361708f266893de5d1769192b60d4b1831f2bb",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5bb0ac23f6e6c4c3ba1b084f2d65cb1bd2a9cf7a",
+   "rev": "221e8088e3a066b8676dc471ff10638cf1c10835",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed250d06b33e67aa5dc5f2cc349a5a35e8b6b390",
+   "rev": "87f6314ff2cc922489cd73cd0fbc2252f39aa153",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0c688ceba0d380f6e56f977009fc2bb2322af5a3",
+   "rev": "3de531c1135f5e3a01f3ac04830996fda476b28e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc3",
+   "inputRev": "v4.29.0-rc6",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«flt-regular»",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc3
+leanprover/lean4:v4.29.0-rc6