Theorem: Ideal.IsLocalization.AtPrime.PID_of_dedekind_domain (FltRegular/NumberTheory/IdealNorm.lean)

State before:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ IsPrincipalIdealRing Aₘ
Tactic:
letI : IsNoetherianRing Aₘ :=
  IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindRing.toIsNoetherian
State after:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
⊢ IsPrincipalIdealRing Aₘ

State before:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
⊢ IsPrincipalIdealRing Aₘ
Tactic:
letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
State after:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
⊢ IsPrincipalIdealRing Aₘ

State before:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
⊢ IsPrincipalIdealRing Aₘ
Tactic:
exact ((tfae_of_isNoetherianRing_of_localRing_of_isDomain Aₘ).out 2 0).mp
  (IsLocalization.AtPrime.isDedekindDomain A P _)
State after:
no goals