those are useless

Author: riccardobrasca

FltRegular/NumberTheory/GaloisPrime.lean

@@ -50,11 +50,6 @@ lemma primesOver_bot [Nontrivial R] [IsDomain S] [NoZeroSMulDivisors R S]
 
 variable (S)
 
-lemma primesOverFinset_bot [IsDedekindDomain S] : primesOverFinset S (⊥ : Ideal R) = ∅ := by
-  classical
-  rw [primesOverFinset, Ideal.map_bot, ← Ideal.zero_eq_bot, factors_zero]
-  rfl
-
 lemma coe_primesOverFinset [Ring.DimensionLEOne R] [IsDedekindDomain S]
     [NoZeroSMulDivisors R S] (p : Ideal R) (hp : p ≠ ⊥) [hp' : p.IsPrime] :
     primesOverFinset S p = primesOver S p := by
@@ -82,14 +77,6 @@ lemma primesOver_finite [Ring.DimensionLEOne R] [IsDedekindDomain S] [NoZeroSMul
   · rw [primesOver_eq_empty_of_not_isPrime S p h]
     exact Set.finite_empty
 
-lemma primesOver_nonempty [IsDomain S] [NoZeroSMulDivisors R S] [Algebra.IsIntegral R S]
-    (p : Ideal R) [p.IsPrime] : (primesOver S p).Nonempty := by
-  have := Ideal.bot_prime (α := S)
-  obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p ⊥
-    (by rw [Ideal.comap_bot_of_injective _
-      (NoZeroSMulDivisors.algebraMap_injective R S)]; exact bot_le)
-  exact ⟨Q, hQ⟩
-
 variable {S}
 
 lemma ne_bot_of_mem_primesOver [IsDedekindDomain S] [NoZeroSMulDivisors R S] {p : Ideal R}

FltRegular/NumberTheory/Hilbert92.lean

@@ -53,15 +53,6 @@ lemma systemOfUnits.IsFundamental.maximal' [Module A G] (S : systemOfUnits p G r
   letI := hs.choose
   convert hs.choose_spec a ‹_› <;> symm <;> exact Nat.card_eq_fintype_card.symm
 
-@[to_additive]
-theorem Finsupp.prod_congr' {α M N} [Zero M] [CommMonoid N] {f₁ f₂ : α →₀ M} {g1 g2 : α → M → N}
-    (h : ∀ x, g1 x (f₁ x) = g2 x (f₂ x)) (hg1 : ∀ i, g1 i 0 = 1) (hg2 : ∀ i, g2 i 0 = 1) :
-    f₁.prod g1 = f₂.prod g2 := by
-  classical
-  rw [f₁.prod_of_support_subset Finset.subset_union_left _ (fun i _ ↦ hg1 i),
-    f₂.prod_of_support_subset Finset.subset_union_right _ (fun i _ ↦ hg2 i)]
-  exact Finset.prod_congr rfl (fun x _ ↦ h x)
-
 @[simps]
 noncomputable
 def Finsupp.ltotal (α M R) [CommSemiring R] [AddCommMonoid M] [Module R M] :

FltRegular/NumberTheory/Unramified.lean

@@ -120,47 +120,10 @@ lemma comap_map_eq_of_isUnramified [IsGalois K L] [IsUnramified R S] (I : Ideal
       Ideal.mem_normalizedFactors_iff hIbot']
     exact ⟨hP.1.comap _, Ideal.comap_mono hP.2⟩
 
-open scoped Classical in
-lemma isUnramifiedAt_iff_normalizedFactors_nodup [NoZeroSMulDivisors R S] [IsDedekindDomain S]
-    (p : Ideal R) [p.IsPrime] (hp : p ≠ ⊥) :
-    IsUnramifiedAt S p ↔ (normalizedFactors (p.map (algebraMap R S))).Nodup := by
-  simp_rw [Multiset.nodup_iff_count_eq_one, ← Multiset.mem_toFinset,
-    ← factors_eq_normalizedFactors]
-  show _ ↔ ∀ P ∈ (primesOverFinset S p : Set (Ideal S)), _
-  simp_rw [IsUnramifiedAt, coe_primesOverFinset S p hp]
-  refine forall₂_congr (fun P hP ↦ ?_)
-  rw [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count]
-  · exact (Ideal.map_eq_bot_iff_of_injective
-      (NoZeroSMulDivisors.algebraMap_injective R S)).not.mpr hp
-  · exact hP.1
-  · exact ne_bot_of_mem_primesOver hp hP
-
 section KummerDedekind
 
 end KummerDedekind
 
-attribute [local instance] Ideal.Quotient.field in
-lemma isUnramifiedAt_iff_SquareFree_minpoly [NoZeroSMulDivisors R S] [IsDedekindDomain S]
-    (p : Ideal R) [hp : p.IsPrime] (hpbot : p ≠ ⊥) (x : S)
-    (hx : (conductor R x).comap (algebraMap R S) ⊔ p = ⊤) (hx' : IsIntegral R x) :
-    IsUnramifiedAt S p ↔ Squarefree ((minpoly R x).map (Ideal.Quotient.mk p)) := by
-  classical
-  have := hp.isMaximal hpbot
-  rw [isUnramifiedAt_iff_normalizedFactors_nodup p hpbot,
-    KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map
-    this hpbot hx hx', Multiset.nodup_map_iff_of_injective, Multiset.nodup_attach,
-    ← squarefree_iff_nodup_normalizedFactors (Polynomial.map_monic_ne_zero (minpoly.monic hx'))]
-  exact Subtype.val_injective.comp
-    (KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
-      this hpbot hx hx').symm.injective
-
-lemma isUnramifiedAt_iff_SquareFree_minpoly_powerBasis [NoZeroSMulDivisors R S] [IsDedekindDomain S]
-    [Algebra.IsIntegral R S] (pb : PowerBasis R S)
-    (p : Ideal R) [p.IsPrime] (hpbot : p ≠ ⊥) :
-    IsUnramifiedAt S p ↔ Squarefree ((minpoly R pb.gen).map (Ideal.Quotient.mk p)) := by
-  rw [isUnramifiedAt_iff_SquareFree_minpoly p hpbot pb.gen _ _]
-  rw [conductor_eq_top_of_powerBasis, Ideal.comap_top, top_sup_eq]
-  exact PowerBasis.isIntegral_gen pb
 
 open nonZeroDivisors Polynomial