valuation rings

Stream: Is there code for X?

[Adam Topaz]

Is there code somewhere for valuation rings? A valuation ring (of a field $F$) is a subring $R$ of a field $F$ satisfying the following property: for all $x \in F$, one has $x \in R$ or $x^{-1} \in R$. I know valuations exists in the perfectoid repo, defined as a map to a totally ordered abelian group, but I couldn't find anything about valuation rings there.

I'm looking for something along the lines of:

class valuation_ring (R : Type*) extends integral_domain R :=
( val_cond : ∀ { x y : R }, ∃ z : R, x * z = y ∨ x = y * z )

[Johan Commelin]

@Adam Topaz We have the valuation ring of an arbitrary valuation. But not the definition that you have in mind. Of course every valuation ring à la your definition is provably also the valuation ring à la perfectoid repo. But this equivalence is not proven there.

[Adam Topaz]

Thanks! I see your definition now in the valuation/localization.lean file.