Localization inside of fraction field

Stream: Is there code for X?

[Adam Topaz]

Suppose I have a domain $A$ and a fraction field $K$ of $A$ (declared in the usual way using [fraction_ring A K].
Suppose I also have a prime ideal $\mathfrak{p}$ of $A$. What's the idiomatic way to consider the localization of $A$ at $\mathfrak{p}$ as a subring of $K$?

[Adam Topaz]

Ideally I would like its carrier to be defeq to

{ x | ∃ (a s : A) (hs : s ∈ P.prime_compl), x = a * s⁻¹ }

[Adam Topaz]

#13425