R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
let P := factors I
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
have prime_of_mem := fun p (hp : p ∈ P.toFinset) =>
  prime_of_factor p (Multiset.mem_toFinset.mp hp)
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Module.IsTorsionBySet R M ↑(⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P)

R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Set.Pairwise ↑(Multiset.toFinset (factors I)) fun i j =>
    (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
apply @torsionBySet_isInternal _ _ _ _ _ _ _ _ (fun p => p ^ P.count p) _
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ (⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P) = I
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Module.IsTorsionBySet R M ↑(⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P)
convert hM
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Associated (Multiset.prod (factors I)) I

case h.e'_6.h.e'_4.prime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R), i ∈ Multiset.toFinset (factors I) → Prime i

case h.e'_6.h.e'_4.coprime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R),
    i ∈ Multiset.toFinset (factors I) → ∀ (j : Ideal R), j ∈ Multiset.toFinset (factors I) → i ≠ j → i ≠ j
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ (⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P) = I
rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_prime_pow_eq_prod, ← Finset.prod_multiset_count,
  ← associated_iff_eq]
no goals
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Associated (Multiset.prod (factors I)) I
exact factors_prod hI
no goals
case h.e'_6.h.e'_4.prime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R), i ∈ Multiset.toFinset (factors I) → Prime i
exact prime_of_mem
no goals
case h.e'_6.h.e'_4.coprime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R),
    i ∈ Multiset.toFinset (factors I) → ∀ (j : Ideal R), j ∈ Multiset.toFinset (factors I) → i ≠ j → i ≠ j
exact fun _ _ _ _ ij => ij
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ (fun p => p ^ Multiset.count p P) p ⊔ (fun p => p ^ Multiset.count p P) q = ⊤
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Set.Pairwise ↑(Multiset.toFinset (factors I)) fun i j =>
    (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤
intro p hp q hq pq
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ Multiset.count p (factors I) ⊔ q ^ Multiset.count q (factors I) = ⊤
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ (fun p => p ^ Multiset.count p P) p ⊔ (fun p => p ^ Multiset.count p P) q = ⊤
dsimp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤

case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ ⊥

case hJ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Irreducible p
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ Multiset.count p (factors I) ⊔ q ^ Multiset.count q (factors I) = ⊤
rw [irreducible_pow_sup]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I))) = 0
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤
suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
no goals
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
this : Multiset.count p (normalizedFactors ?m.89951) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤
rw [this, zero_min, pow_zero, Ideal.one_eq_top]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ ¬(Multiset.count q (factors I) ≠ 0 ∧ p = ↑normalize q)
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I))) = 0
rw [Multiset.count_eq_zero,
  normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
  Multiset.mem_replicate]
no goals
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ ¬(Multiset.count q (factors I) ≠ 0 ∧ p = ↑normalize q)
exact fun H => pq <| H.2.trans <| normalize_eq q
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ 0
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ ⊥
rw [← Ideal.zero_eq_bot]
case hI.h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ≠ 0
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ 0
apply pow_ne_zero
no goals
case hI.h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ≠ 0
exact (prime_of_mem q hq).ne_zero
no goals
case hJ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Irreducible p
exact (prime_of_mem p hp).irreducible