let's get rid of this

leanprover-community · Jul 5, 2024 · ef78720 · ef78720
1 parent 2f9431b
commit ef78720
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 12 deletions.
diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
@@ -87,11 +87,10 @@ lemma isCoprime_of_not_zeta_sub_one_dvd (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x)
     Ideal.mem_span_singleton]
   · simpa only [ge_iff_le, tsub_pos_iff_lt] using hpri.out.one_lt
 
-set_option synthInstance.maxHeartbeats 80000 in
-lemma exists_zeta_sub_one_dvd_sub_Int (a : 𝓞 K) : ∃ b : ℤ, (hζ.unit' - 1: 𝓞 K) ∣ a - b := by
-  letI : AddGroup (𝓞 K ⧸ Ideal.span (singleton (hζ.unit' - 1: 𝓞 K))) := inferInstance
+lemma exists_zeta_sub_one_dvd_sub_Int (a : 𝓞 K) : ∃ b : ℤ, (hζ.unit' - 1 : 𝓞 K) ∣ a - b := by
   letI : Fact (Nat.Prime p) := hpri
-  simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, map_sub, sub_eq_zero, ← SModEq.Ideal_def]
+  simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_sub,
+    sub_eq_zero, ← SModEq.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]

diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean
@@ -39,11 +39,3 @@ theorem exists_int_sModEq (x : 𝓞 K) :
     rw [SModEq.sub_mem, mul_one, add_sub_cancel_left, mul_comm, mem_span_singleton']
     exact ⟨_, rfl⟩
   · exact not_mem_erase (⟨0, pb.dim_pos⟩ : Fin pb.dim) univ
-
-variable [NumberField K] {pb}
-
-variable (hpr : Prime (norm ℚ pb.gen))
-
-lemma SModEq.Ideal_def {R : Type*} [CommRing R] (I : Ideal R) (x y : R) :
-  x ≡ y [SMOD I] ↔ Ideal.Quotient.mk I x = Ideal.Quotient.mk I y :=
-Iff.rfl