no goals
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ DiscreteValuationRing Aₘ
classical
letI : IsNoetherianRing Aₘ :=
  IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindDomain.isNoetherianRing
letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
exact
  ((DiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
    (IsLocalization.AtPrime.isDedekindDomain A P _)
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.isNoetherianRing
⊢ DiscreteValuationRing Aₘ
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ DiscreteValuationRing Aₘ
letI : IsNoetherianRing Aₘ :=
  IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindDomain.isNoetherianRing
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.isNoetherianRing
this : LocalRing Aₘ := localRing Aₘ P
⊢ DiscreteValuationRing Aₘ
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.isNoetherianRing
⊢ DiscreteValuationRing Aₘ
letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.isNoetherianRing
this : LocalRing Aₘ := localRing Aₘ P
hnf : ¬IsField Aₘ
⊢ DiscreteValuationRing Aₘ
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.isNoetherianRing
this : LocalRing Aₘ := localRing Aₘ P
⊢ DiscreteValuationRing Aₘ
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
no goals
R : Type ?u.45003
A : Type u_1
K : Type ?u.45009
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : Field K
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : Ideal.IsPrime P
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing (Ideal.primeCompl P) Aₘ IsDedekindDomain.isNoetherianRing
this : LocalRing Aₘ := localRing Aₘ P
hnf : ¬IsField Aₘ
⊢ DiscreteValuationRing Aₘ
exact
  ((DiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
    (IsLocalization.AtPrime.isDedekindDomain A P _)