fix: remove DecidableEq assumption from factors (#11158)

It doesn't make a lot of sense for `factors` to require a `DecidableEq` assumption since it's not used in the statement, and the definition is already noncomputable. This PR removes that assumption and updates some lemmas later in the file accordingly.

Mathlib/RingTheory/ChainOfDivisors.lean

@@ -249,8 +249,8 @@ variable [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M]
 open DivisorChain
 
 theorem pow_image_of_prime_by_factor_orderIso_dvd
-    [DecidableEq (Associates M)] {m p : Associates M} {n : Associates N} (hn : n ≠ 0)
-    (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) {s : ℕ} (hs' : p ^ s ≤ m) :
+    {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m)
+    (d : Set.Iic m ≃o Set.Iic n) {s : ℕ} (hs' : p ^ s ≤ m) :
     (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ^ s ≤ n := by
   by_cases hs : s = 0
   · simp [hs]
@@ -280,8 +280,8 @@ theorem pow_image_of_prime_by_factor_orderIso_dvd
   exact ne_zero_of_dvd_ne_zero hn (Subtype.prop (d ⟨c₁ 1 ^ s, _⟩))
 #align pow_image_of_prime_by_factor_order_iso_dvd pow_image_of_prime_by_factor_orderIso_dvd
 
-theorem map_prime_of_factor_orderIso [DecidableEq (Associates M)] {m p : Associates M}
-    {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
+theorem map_prime_of_factor_orderIso {m p : Associates M} {n : Associates N} (hn : n ≠ 0)
+    (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
     Prime (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) := by
   rw [← irreducible_iff_prime]
   refine' (Associates.isAtom_iff <| ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨_, fun b hb => _⟩
@@ -307,9 +307,8 @@ theorem map_prime_of_factor_orderIso [DecidableEq (Associates M)] {m p : Associa
     simp
 #align map_prime_of_factor_order_iso map_prime_of_factor_orderIso
 
-theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors [DecidableEq (Associates M)]
-    [DecidableEq (Associates N)] {m p : Associates M} {n : Associates N} (hn : n ≠ 0)
-    (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
+theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors {m p : Associates M}
+    {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
     (d ⟨p, dvd_of_mem_normalizedFactors hp⟩ : Associates N) ∈ normalizedFactors n := by
   obtain ⟨q, hq, hq'⟩ :=
     exists_mem_normalizedFactors_of_dvd hn (map_prime_of_factor_orderIso hn hp d).irreducible
@@ -320,9 +319,8 @@ theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors [Decidabl
 
 variable [DecidableRel ((· ∣ ·) : M → M → Prop)] [DecidableRel ((· ∣ ·) : N → N → Prop)]
 
-theorem multiplicity_prime_le_multiplicity_image_by_factor_orderIso [DecidableEq (Associates M)]
-    {m p : Associates M} {n : Associates N} (hp : p ∈ normalizedFactors m)
-    (d : Set.Iic m ≃o Set.Iic n) :
+theorem multiplicity_prime_le_multiplicity_image_by_factor_orderIso {m p : Associates M}
+    {n : Associates N} (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
     multiplicity p m ≤ multiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n := by
   by_cases hn : n = 0
   · simp [hn]
@@ -335,9 +333,8 @@ theorem multiplicity_prime_le_multiplicity_image_by_factor_orderIso [DecidableEq
   exact pow_image_of_prime_by_factor_orderIso_dvd hn hp d (pow_multiplicity_dvd _)
 #align multiplicity_prime_le_multiplicity_image_by_factor_order_iso multiplicity_prime_le_multiplicity_image_by_factor_orderIso
 
-theorem multiplicity_prime_eq_multiplicity_image_by_factor_orderIso [DecidableEq (Associates M)]
-    {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m)
-    (d : Set.Iic m ≃o Set.Iic n) :
+theorem multiplicity_prime_eq_multiplicity_image_by_factor_orderIso {m p : Associates M}
+    {n : Associates N} (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) (d : Set.Iic m ≃o Set.Iic n) :
     multiplicity p m = multiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n := by
   refine' le_antisymm (multiplicity_prime_le_multiplicity_image_by_factor_orderIso hp d) _
   suffices multiplicity (↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩)) n ≤
@@ -389,11 +386,10 @@ def mkFactorOrderIsoOfFactorDvdEquiv {m : M} {n : N} {d : { l : M // l ∣ m } 
         Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff, mk_out]
 #align mk_factor_order_iso_of_factor_dvd_equiv mkFactorOrderIsoOfFactorDvdEquiv
 
-variable [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N] [DecidableEq M]
+variable [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N]
 
-theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors [DecidableEq N] {m p : M}
-    {n : N} (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ normalizedFactors m)
-    {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }}
+theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors {m p : M} {n : N} (hm : m ≠ 0)
+    (hn : n ≠ 0) (hp : p ∈ normalizedFactors m) {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }}
     (hd : ∀ l l', (d l : N) ∣ d l' ↔ (l : M) ∣ (l' : M)) :
     ↑(d ⟨p, dvd_of_mem_normalizedFactors hp⟩) ∈ normalizedFactors n := by
   suffices
@@ -445,7 +441,6 @@ theorem multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalizedFactors {m
       exact mk_le_mk_of_dvd (dvd_of_mem_normalizedFactors hp)⟩) :=
     by rw [mkFactorOrderIsoOfFactorDvdEquiv_apply_coe]
   rw [this]
-  letI := Classical.decEq (Associates M)
   refine'
     multiplicity_prime_eq_multiplicity_image_by_factor_orderIso (mk_ne_zero.mpr hn) _
       (mkFactorOrderIsoOfFactorDvdEquiv hd)

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -746,7 +746,6 @@ open UniqueFactorizationMonoid
 
 theorem Ideal.eq_prime_pow_of_succ_lt_of_le {P I : Ideal A} [P_prime : P.IsPrime] (hP : P ≠ ⊥)
     {i : ℕ} (hlt : P ^ (i + 1) < I) (hle : I ≤ P ^ i) : I = P ^ i := by
-  have := Classical.decEq (Ideal A)
   refine le_antisymm hle ?_
   have P_prime' := Ideal.prime_of_isPrime hP P_prime
   have h1 : I ≠ ⊥ := (lt_of_le_of_lt bot_le hlt).ne'
@@ -889,8 +888,7 @@ theorem inf_eq_mul_of_coprime {I J : Ideal A} (coprime : IsCoprime I J) : I ⊓
 theorem isCoprime_iff_gcd {I J : Ideal A} : IsCoprime I J ↔ gcd I J = 1 := by
   rw [Ideal.isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]
 
-theorem factors_span_eq [DecidableEq K[X]] [DecidableEq (Ideal K[X])] {p : K[X]} :
-    factors (span {p}) = (factors p).map (fun q ↦ span {q}) := by
+theorem factors_span_eq {p : K[X]} : factors (span {p}) = (factors p).map (fun q ↦ span {q}) := by
   rcases eq_or_ne p 0 with rfl | hp; · simpa [Set.singleton_zero] using normalizedFactors_zero
   have : ∀ q ∈ (factors p).map (fun q ↦ span {q}), Prime q := fun q hq ↦ by
     obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
@@ -1442,7 +1440,7 @@ theorem Ideal.squarefree_span_singleton {a : R} :
     exact isUnit_iff.mpr <| eq_top_of_isUnit_mem _ (Submodule.IsPrincipal.generator_mem I) (h _ hI)
 
 theorem singleton_span_mem_normalizedFactors_of_mem_normalizedFactors [NormalizationMonoid R]
-    [DecidableEq R] [DecidableEq (Ideal R)] {a b : R} (ha : a ∈ normalizedFactors b) :
+    {a b : R} (ha : a ∈ normalizedFactors b) :
     Ideal.span ({a} : Set R) ∈ normalizedFactors (Ideal.span ({b} : Set R)) := by
   by_cases hb : b = 0
   · rw [Ideal.span_singleton_eq_bot.mpr hb, bot_eq_zero, normalizedFactors_zero]

Mathlib/RingTheory/DedekindDomain/PID.lean

@@ -211,9 +211,8 @@ variable [IsDomain Sₚ] [IsDedekindDomain Sₚ]
 
 /-- If `p` is a prime in the Dedekind domain `R`, `S` an extension of `R` and `Sₚ` the localization
 of `S` at `p`, then all primes in `Sₚ` are factors of the image of `p` in `Sₚ`. -/
-theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime [DecidableEq (Ideal Sₚ)]
-    {P : Ideal Sₚ} (hP : IsPrime P) (hP0 : P ≠ ⊥) :
-    P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p) := by
+theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime {P : Ideal Sₚ} (hP : IsPrime P)
+    (hP0 : P ≠ ⊥) : P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p) := by
   have non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
     map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _)
       p.primeCompl_le_nonZeroDivisors