clean more stuff

FltRegular/FltThree/Edwards.lean

@@ -380,26 +380,6 @@ theorem factorization'.associated'_of_norm_associated {a b c : ℤ√(-3)} (h :
   · exact factorization'.coprime_of_mem h hcmem
   · exact ((factorization'_prop h).2 b hbmem).2.2
 
-theorem factors_unique {f g : Multiset (ℤ√(-3))} (hf : ∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs)
-    (hf' : ∀ x ∈ f, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x))
-    (hg : ∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs)
-    (hg' : ∀ x ∈ g, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x)) (h : Associated f.prod g.prod) :
-    Multiset.Rel Associated' f g :=
-  by
-  have p :
-    ∀ (x : ℤ√(-3)) (_ : x ∈ f) (y : ℤ√(-3)) (_ : y ∈ g),
-      (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y :=
-    by
-    intro x hx y hy hxy
-    rw [Function.comp_apply, Function.comp_apply, ← Int.associated_iff_natAbs] at hxy
-    apply associated'_of_associated_norm hxy
-    · exact hf' x hx
-    · exact hg' y hy
-    · exact hf x hx
-  refine' Multiset.Rel.mono _ p
-  rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h,
-    Multiset.rel_eq]
-
 theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
     Even (evenFactorExp a.norm.natAbs) :=
   by

FltRegular/FltThree/OddPrimeOrFour.lean

@@ -129,13 +129,6 @@ theorem oddFactors.pow (z : ℕ) (n : ℕ) : oddFactors (z ^ n) = n • oddFacto
 noncomputable def evenFactorExp (x : ℕ) :=
   Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x)
 
-theorem evenFactorExp.def (x : ℕ) :
-    evenFactorExp x = Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) :=
-  rfl
-
-theorem evenFactorExp.zero : evenFactorExp 0 = 0 := by
-  simp [evenFactorExp]
-
 theorem evenFactorExp.pow (z : ℕ) (n : ℕ) : evenFactorExp (z ^ n) = n * evenFactorExp z :=
   by
   simp only [evenFactorExp]
@@ -170,13 +163,6 @@ theorem even_and_odd_factors' (x : ℕ) :
   convert even_and_odd_factors'' x
   simp [evenFactorExp, ← Multiset.filter_eq]
 
-theorem even_and_oddFactors (x : ℕ) (hx : x ≠ 0) :
-    Associated x (2 ^ evenFactorExp x * (oddFactors x).prod) :=
-  by
-  convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm
-  simp [evenFactorExp]
-  rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x]
-
 theorem factors_2_even {z : ℕ} (hz : z ≠ 0) : evenFactorExp (4 * z) = 2 + evenFactorExp z :=
   by
   have h₀ : (4 : ℕ) ≠ 0 := four_ne_zero

FltRegular/FltThree/Spts.lean

@@ -406,12 +406,3 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs
     _ = 1 := by
       rw [hfour]
       norm_num
-
-
-theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hfour : p.norm = 4) :
-    abs p.re = 1 ∧ abs p.im = 1 := by
-  apply Spts.four hfour
-  rintro him
-  rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
-  rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour
-  norm_num at hfour

FltRegular/NumberTheory/CyclotomicRing.lean

@@ -124,11 +124,5 @@ lemma charZero {p} (hp : p ≠ 0) : CharZero (CyclotomicIntegers p) :=
 
 instance : CharZero (CyclotomicIntegers p) := charZero hpri.out.ne_zero
 
-open BigOperators
-
-lemma sum_zeta_pow : ∑ i in Finset.range p, zeta p ^ (i : ℕ) = 0 := by
-  rw [← AdjoinRoot.aeval_root (Polynomial.cyclotomic p ℤ), ← zeta]
-  simp [Polynomial.cyclotomic_prime ℤ p]
-
 end CyclotomicIntegers
 end

FltRegular/NumberTheory/IdealNorm.lean

@@ -97,19 +97,19 @@ theorem spanIntNorm_singleton {r : S} :
           exact map_dvd _ (mem_span_singleton.mp hx')))
     ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanIntNorm _ _ (mem_span_singleton_self _)))
 
-@[simp]
-theorem spanIntNorm_top : spanIntNorm R (⊤ : Ideal S) = ⊤ := by
-  rw [← Ideal.span_singleton_one, spanIntNorm_singleton]
-  simp
+-- @[simp]
+-- theorem spanIntNorm_top : spanIntNorm R (⊤ : Ideal S) = ⊤ := by
+--   rw [← Ideal.span_singleton_one, spanIntNorm_singleton]
+--   simp
 
 theorem map_spanIntNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
     map f (spanIntNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) := by
   rw [spanIntNorm, map_span, Set.image_image]
   rfl
 
-@[mono]
-theorem spanIntNorm_mono {I J : Ideal S} (h : I ≤ J) : spanIntNorm R I ≤ spanIntNorm R J :=
-  Ideal.span_mono (Set.monotone_image h)
+-- @[mono]
+-- theorem spanIntNorm_mono {I J : Ideal S} (h : I ≤ J) : spanIntNorm R I ≤ spanIntNorm R J :=
+--   Ideal.span_mono (Set.monotone_image h)
 
 theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰)
     {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ]
@@ -179,21 +179,21 @@ theorem spanIntNorm_mul_spanIntNorm_le (I J : Ideal S) :
   rintro _ ⟨x, hxI, y, hyJ, rfl⟩
   exact Ideal.mul_mem_mul hxI hyJ
 
-/-- This condition `eq_bot_or_top` is equivalent to being a field.
-However, `Ideal.spanIntNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
-instance to a `Field R` instance. -/
-theorem spanIntNorm_mul_of_bot_or_top [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S]
-    (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
-    spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J := by
-  refine le_antisymm ?_ (spanIntNorm_mul_spanIntNorm_le R _ _)
-  cases' eq_bot_or_top (spanIntNorm R I) with hI hI
-  · rw [hI, spanIntNorm_eq_bot_iff.mp hI, bot_mul, spanIntNorm_bot]
-    exact bot_le
-  rw [hI, Ideal.top_mul]
-  cases' eq_bot_or_top (spanIntNorm R J) with hJ hJ
-  · rw [hJ, spanIntNorm_eq_bot_iff.mp hJ, mul_bot, spanIntNorm_bot]
-  rw [hJ]
-  exact le_top
+-- /-- This condition `eq_bot_or_top` is equivalent to being a field.
+-- However, `Ideal.spanIntNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
+-- instance to a `Field R` instance. -/
+-- theorem spanIntNorm_mul_of_bot_or_top [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S]
+--     (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
+--     spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J := by
+--   refine le_antisymm ?_ (spanIntNorm_mul_spanIntNorm_le R _ _)
+--   cases' eq_bot_or_top (spanIntNorm R I) with hI hI
+--   · rw [hI, spanIntNorm_eq_bot_iff.mp hI, bot_mul, spanIntNorm_bot]
+--     exact bot_le
+--   rw [hI, Ideal.top_mul]
+--   cases' eq_bot_or_top (spanIntNorm R J) with hJ hJ
+--   · rw [hJ, spanIntNorm_eq_bot_iff.mp hJ, mul_bot, spanIntNorm_bot]
+--   rw [hJ]
+--   exact le_top
 
 variable [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S]
 

FltRegular/NumberTheory/RegularPrimes.lean

@@ -56,15 +56,6 @@ def IsRegularNumber [hn : Fact (0 < n)] : Prop :=
 def IsRegularPrime : Prop :=
   IsRegularNumber p
 
-/-- A prime number is Bernoulli regular if it does not divide the numerator of any of
-the first `p - 3` (non-zero) Bernoulli numbers-/
-def IsBernoulliRegular : Prop :=
-  ∀ i ∈ Finset.range ((p - 3) / 2), ((bernoulli 2 * i).num : ZMod p) ≠ 0
-
-/-- A prime is super regular if its regular and Bernoulli regular.-/
-def IsSuperRegular : Prop :=
-  IsRegularNumber p ∧ IsBernoulliRegular p
-
 section TwoRegular
 
 variable (A K : Type _) [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K]