SchemeTheory.localizationAtPrime_isDiscreteValuationRing
The native prime localization of a Dedekind domain is a DVR at a nonzero prime. Its coefficient Algebra stays inside this ring-only owner.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace SchemeTheory
universe uLean source · statement
theorem localizationAtPrime_isDiscreteValuationRing
(B : Type u) [CommRing B] [IsDedekindDomain B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) :
IsDiscreteValuationRing (Localization.AtPrime Q)