bump

FltRegular/MayAssume/Lemmas.lean

@@ -1,7 +1,6 @@
 import FltRegular.FltThree.FltThree
 import Mathlib.Algebra.GCDMonoid.Finset
 import Mathlib.FieldTheory.Finite.Basic
-import Mathlib.Algebra.GCDMonoid.Div
 import FltRegular.NumberTheory.RegularPrimes
 
 open Int Finset
@@ -39,7 +38,7 @@ theorem coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a *
       Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero,
       Int.mul_ediv_cancel_left _ hdzero, mul_comm, ← hna, mul_comm, ← hnb, mul_comm, ← hnc]
   · simpa [gcd_eq_gcd_image, d] using
-      Finset.Int.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
+      Finset.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
   · simp only [mul_eq_zero] at habs
     rcases habs with ((Ha | Hb) | Hc)
     · exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha)

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -114,8 +114,6 @@ instance a3 : NumberField (CyclotomicField p ℚ) :=
 
 open IsPrimitiveRoot
 
-attribute [-instance] CharP.CharOne.subsingleton
-
 theorem nth_roots_prim [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) :
     IsPrimitiveRoot η p := by
   have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe

FltRegular/NumberTheory/Hilbert92.lean

@@ -733,7 +733,6 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
       congr
       rw [hE]
       field_simp
-      rw [mul_comm]
   rw [norm_eq_prod_pow_gen σ hσ, orderOf_eq_card_of_forall_mem_zpowers hσ,
     IsGalois.card_aut_eq_finrank, hKL]
   conv =>

lake-manifest.json

@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "0e991536465f9d37d4c0f73e1d2dd7bcde989e80",
+   "rev": "e9bc16347b34a91a7498edb615179b5788bf1ed4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,