bump

leanprover-community · Feb 17, 2025 · fd4ffd5 · fd4ffd5
1 parent 1d5b6eb
commit fd4ffd5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -114,8 +114,9 @@ open IsPrimitiveRoot
 
 theorem nth_roots_prim [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) :
     IsPrimitiveRoot η p := by
+  classical
   have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe
-  rw [nthRoots_one_eq_biUnion_primitiveRoots hζ'] at hη
+  rw [nthRoots_one_eq_biUnion_primitiveRoots] at hη
   simp only [mem_biUnion] at hη
   obtain ⟨a, ha, h2⟩ := hη
   have ha2 : a = p := by

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "854a2aadc4dbdf8bc32e0ae63b98d470ef3e71f4",
+   "rev": "981a86e7f2342cd84acac36c2ec4016f87ae54b6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b18855cb0f9a19bd4d7e21f3e5525272e377f431",
+   "rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",