feat(ring_theory/dedekind_domain/ideal): drop an unneeded assumption (#14444)

Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Author: urkud

src/ring_theory/dedekind_domain/ideal.lean

@@ -673,6 +673,13 @@ theorem ideal.prime_iff_is_prime {P : ideal A} (hP : P ≠ ⊥) :
   prime P ↔ is_prime P :=
 ⟨ideal.is_prime_of_prime, ideal.prime_of_is_prime hP⟩
 
+/-- In a Dedekind domain, the the prime ideals are the zero ideal together with the prime elements
+of the monoid with zero `ideal A`. -/
+theorem ideal.is_prime_iff_bot_or_prime {P : ideal A} :
+  is_prime P ↔ P = ⊥ ∨ prime P :=
+⟨λ hp, (eq_or_ne P ⊥).imp_right $ λ hp0, (ideal.prime_of_is_prime hp0 hp),
+ λ hp, hp.elim (λ h, h.symm ▸ ideal.bot_prime) ideal.is_prime_of_prime⟩
+
 lemma ideal.strict_anti_pow (I : ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) :
   strict_anti ((^) I : ℕ → ideal A) :=
 strict_anti_nat_of_succ_lt $ λ e, ideal.dvd_not_unit_iff_lt.mp
@@ -899,10 +906,11 @@ section
 
 open_locale classical
 
-lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
+lemma ideal.count_normalized_factors_eq {p x : ideal R} [hp : p.is_prime] {n : ℕ}
   (hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
   (normalized_factors x).count p = n :=
-count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible
+count_normalized_factors_eq'
+  ((ideal.is_prime_iff_bot_or_prime.mp hp).imp_right prime.irreducible)
   (by { haveI : unique (ideal R)ˣ := ideal.unique_units, apply normalize_eq })
   (by convert ideal.dvd_iff_le.mpr hle) (by convert mt ideal.le_of_dvd hlt)
 /- Warning: even though a pure term-mode proof typechecks (the `by convert` can simply be

src/ring_theory/unique_factorization_domain.lean

@@ -783,6 +783,7 @@ begin
 end
 
 omit dec_dvd
+
 /-- The number of times an irreducible factor `p` appears in `normalized_factors x` is defined by
 the number of times it divides `x`.
 
@@ -801,6 +802,24 @@ begin
   exact (multiplicity.eq_coe_iff.mpr ⟨hle, hlt⟩).symm
 end
 
+/-- The number of times an irreducible factor `p` appears in `normalized_factors x` is defined by
+the number of times it divides `x`. This is a slightly more general version of
+`unique_factorization_monoid.count_normalized_factors_eq` that allows `p = 0`.
+
+See also `multiplicity_eq_count_normalized_factors` if `n` is given by `multiplicity p x`.
+-/
+lemma count_normalized_factors_eq' {p x : R} (hp : p = 0 ∨ irreducible p) (hnorm : normalize p = p)
+  {n : ℕ} (hle : p^n ∣ x) (hlt : ¬ (p^(n+1) ∣ x)) :
+  (normalized_factors x).count p = n :=
+begin
+  rcases hp with rfl|hp,
+  { cases n,
+    { exact count_eq_zero.2 (zero_not_mem_normalized_factors _) },
+    { rw [zero_pow (nat.succ_pos _)] at hle hlt,
+      exact absurd hle hlt } },
+  { exact count_normalized_factors_eq hp hnorm hle hlt }
+end
+
 end multiplicity
 
 end unique_factorization_monoid