bump

FltRegular/CaseI/Statement.lean

@@ -250,7 +250,7 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
     singleton_subset_iff.2 (mem_range.2 (Fin.is_lt _))⟩⟩⟩
   have hcard := card_sdiff hs
   replace hcard : (range p \ s).Nonempty
-  · rw [← card_pos, hcard, card_range]
+  · rw [← Finset.card_pos, hcard, card_range]
     exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
   obtain ⟨i, hi⟩ := hcard
   refine' ⟨i, sdiff_subset _ _ hi, _⟩

FltRegular/CaseII/AuxLemmas.lean

@@ -170,7 +170,7 @@ lemma IsPrimitiveRoot.prime_span_sub_one : Prime (Ideal.span <| singleton <| (h
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   rw [Ideal.prime_iff_isPrime,
     Ideal.span_singleton_prime (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)]
-  exact IsCyclotomicExtension.Rat.zeta_sub_one_prime' hζ hp
+  exact hζ.zeta_sub_one_prime'
   · rw [Ne.def, Ideal.span_singleton_eq_bot]
     exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt
 
@@ -202,7 +202,7 @@ lemma isCoprime_of_not_zeta_sub_one_dvd (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x)
   rwa [← Ideal.isCoprime_span_singleton_iff,
     ← Ideal.span_singleton_eq_span_singleton.mpr (associated_zeta_sub_one_pow_prime hζ),
     ← Ideal.span_singleton_pow, IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd,
-    (hζ.prime_span_sub_one hp).irreducible.gcd_eq_one_iff, Ideal.dvd_span_singleton,
+    hζ.prime_span_sub_one.irreducible.gcd_eq_one_iff, Ideal.dvd_span_singleton,
     Ideal.mem_span_singleton]
   · simpa only [ge_iff_le, tsub_pos_iff_lt] using hpri.out.one_lt
 
@@ -212,7 +212,7 @@ lemma exists_zeta_sub_one_dvd_sub_Int (a : 𝓞 K) : ∃ b : ℤ, (hζ.unit' - 1
   simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, map_sub, sub_eq_zero, ← SModEq.Ideal_def]
   convert exists_int_sModEq hζ.subOneIntegralPowerBasis' a
   rw [hζ.subOneIntegralPowerBasis'_gen]
-  rw [Subtype.ext_iff, AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one]
+  rw [Subtype.ext_iff, AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, AddSubgroupClass.coe_sub, OneMemClass.coe_one]
 
 lemma exists_dvd_pow_sub_Int_pow (a : 𝓞 K) : ∃ b : ℤ, ↑p ∣ a ^ (p : ℕ) - (b : 𝓞 K) ^ (p : ℕ) := by
   obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root ℚ (B := K) (Set.mem_singleton p)

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -3,7 +3,6 @@ import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
 import Mathlib.NumberTheory.Cyclotomic.Rat
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import Mathlib.RingTheory.DedekindDomain.Ideal
-import FltRegular.ReadyForMathlib.ZetaSubOnePrime
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
 import Mathlib.Algebra.CharP.Quotient
 
@@ -21,6 +20,8 @@ noncomputable section
 
 open scoped NumberField BigOperators
 
+instance {K : Type*} [Field K] : Module (𝓞 K) (𝓞 K) := Semiring.toModule
+
 open Ideal IsCyclotomicExtension
 
 -- TODO can we make a relative version of this with another base ring instead of ℤ ?
@@ -193,18 +194,10 @@ theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη :
   norm_cast at h2
   simp [h2]
 
-theorem one_sub_zeta_prime [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη : η ∈ nthRootsFinset p R)
+theorem one_sub_zeta_prime [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R)
     (hne1 : η ≠ 1) : Prime (1 - η) := by
-  replace ph : p ≠ 2
-  · intro h
-    rw [h] at ph
-    simp at ph
   have h := prim_coe η (nth_roots_prim hη hne1)
-  have := Rat.zeta_sub_one_prime' h ph
-  have H :
-    (⟨η - 1, Subalgebra.sub_mem _ (h.isIntegral p.pos) (Subalgebra.one_mem _)⟩ : R) = η - 1 := rfl
-  rw [H] at this
-  simpa using this.neg
+  simpa using h.zeta_sub_one_prime'.neg
 
 theorem diff_of_roots [hp : Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R}
     (hη₁ : η₁ ∈ nthRootsFinset p R) (hη₂ : η₂ ∈ nthRootsFinset p R) (hdiff : η₁ ≠ η₂)
@@ -282,7 +275,7 @@ lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ}
     have eta_sub_one_ne_zero := sub_ne_zero.mpr (Ne.symm hwlog)
     have hηprime : IsPrime (Ideal.span ({1 - η₁} : Set R)) := by
       rw [span_singleton_prime eta_sub_one_ne_zero]
-      apply one_sub_zeta_prime ph hη₁ hwlog
+      apply one_sub_zeta_prime hη₁ hwlog
     have H5 : IsPrime (Ideal.span ({(p : ℤ)} : Set ℤ)) := by
       have h2 : (p : ℤ) ≠ 0 := by simp
       have h1 : Prime (p : ℤ) := by
@@ -409,9 +402,9 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     congr; rfl; ext x
     rw [smul_neg]
     congr; congr; rfl; congr
-    rw [hcoe, ← hζ'.integralPowerBasis'_gen, ← hb]
+    rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
     rfl; rfl; congr; congr; rfl; congr
-    rw [hcoe, ← hζ'.integralPowerBasis'_gen, ← hb]
+    rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
   conv_lhs at hy =>
     congr; rfl; ext x
     rw [← SubsemiringClass.coe_pow, ← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y,
@@ -461,9 +454,9 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
     congr; rfl; ext x
     rw [smul_neg]
     congr; congr; rfl; congr
-    rw [hcoe, ← hζ'.integralPowerBasis'_gen, ← hb]
+    rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
     rfl; rfl; congr; congr; rfl; congr
-    rw [hcoe, ← hζ'.integralPowerBasis'_gen, ← hb]
+    rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
   conv_lhs at hy =>
     congr; rfl; ext x
     rw [← SubsemiringClass.coe_pow, ← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y,

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -1,8 +1,7 @@
 import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
-import Mathlib.RingTheory.RootsOfUnity.Basic
+import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.NumberField.Embeddings
-import FltRegular.ReadyForMathlib.ZetaSubOnePrime
 
 variable {p : ℕ+} {K : Type _} [Field K]
 
@@ -305,10 +304,10 @@ theorem norm_cast_ne_two (h : p ≠ 2) : (p : ℕ) ≠ 2 := by
   contrapose! h
   exact PNat.coe_injective h
 
-theorem IsPrimitiveRoot.isPrime_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h : p ≠ 2) :
+theorem IsPrimitiveRoot.isPrime_one_sub_zeta [hp : Fact (p : ℕ).Prime] :
     (I : Ideal (𝓞 K)).IsPrime := by
   rw [Ideal.span_singleton_prime]
-  · exact IsCyclotomicExtension.Rat.zeta_sub_one_prime' hζ h
+  · exact hζ.zeta_sub_one_prime'
   apply_fun (fun x : 𝓞 K => (x : K))
   push_cast
   rw [Ne.def, sub_eq_zero]
@@ -324,7 +323,7 @@ theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h
   intro h2m
   have := Ideal.sub_mem I hpm (Ideal.mul_mem_right (↑k) I h2m)
   rw [sub_eq_of_eq_add hk] at this
-  exact (hζ.isPrime_one_sub_zeta h).ne_top (Ideal.eq_top_of_isUnit_mem I this isUnit_one)
+  exact hζ.isPrime_one_sub_zeta.ne_top (Ideal.eq_top_of_isUnit_mem I this isUnit_one)
 
 lemma IsUnit.eq_mul_left_iff {S : Type*} [CommRing S] {x : S} (hx : IsUnit x) (y : S) :
   x = y * x ↔ y = 1 := by

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "81dd376a02781030ead59ee35ca5334a7fccc527",
+    "rev": "5f066e77432aee5c14c229c3aaa178ff639be1a2",
     "opts": {},
     "name": "mathlib",
     "inputRev?": null,
@@ -20,7 +20,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "869c615eb10130c0637a7bc038e2b80253559913",
+    "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227",
     "opts": {},
     "name": "std",
     "inputRev?": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.3.0-rc1