R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
⊢ IsPrincipalIdealRing Sₚ
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
⊢ IsPrincipalIdealRing Sₚ
letI := Classical.decEq (Ideal Sₚ)
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
⊢ IsPrincipalIdealRing Sₚ
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
⊢ IsPrincipalIdealRing Sₚ
letI := Classical.decPred fun P : Ideal Sₚ => P.IsPrime
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
P : Ideal Sₚ
⊢ P ∈ Finset.filter (fun P => IsPrime P) ({⊥} ∪ Multiset.toFinset (normalizedFactors (map (algebraMap R Sₚ) p))) ↔
    P ∈ {I | IsPrime I}
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
⊢ IsPrincipalIdealRing Sₚ
refine'
  IsPrincipalIdealRing.of_finite_primes
    (Set.Finite.ofFinset
      (Finset.filter (fun P => P.IsPrime)
        ({⊥} ∪ (normalizedFactors (Ideal.map (algebraMap R Sₚ) p)).toFinset))
      fun P => _)
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
P : Ideal Sₚ
⊢ (P = ⊥ ∨ P ∈ normalizedFactors (map (algebraMap R Sₚ) p)) ∧ IsPrime P ↔ IsPrime P
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
P : Ideal Sₚ
⊢ P ∈ Finset.filter (fun P => IsPrime P) ({⊥} ∪ Multiset.toFinset (normalizedFactors (map (algebraMap R Sₚ) p))) ↔
    P ∈ {I | IsPrime I}
rw [Finset.mem_filter, Finset.mem_union, Finset.mem_singleton, Set.mem_setOf,
  Multiset.mem_toFinset]
no goals
R : Type ?u.282964
inst✝¹⁵ : CommRing R
inst✝¹⁴ : IsDomain R
inst✝¹³ : IsDedekindDomain R
S : Type ?u.283172
inst✝¹² : CommRing S
inst✝¹¹ : IsDomain S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module.Free R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : IsPrime p
Sₚ : Type u_1
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S (primeCompl p)) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDomain Sₚ
inst✝ : IsDedekindDomain Sₚ
this✝ : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun P => IsPrime P := Classical.decPred fun P => IsPrime P
P : Ideal Sₚ
⊢ (P = ⊥ ∨ P ∈ normalizedFactors (map (algebraMap R Sₚ) p)) ∧ IsPrime P ↔ IsPrime P
exact
  and_iff_right_of_imp fun hP =>
    or_iff_not_imp_left.mpr (IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime S p hp0 hP)