Localization of ordered integral domains

Stream: Is there code for X?

[Apurva Nakade]

Are there any results in the library saying that the localization of an ordered integral domain naturally gets an induced ordered integral domain structure?

[Apurva Nakade]

I did a Ctrl+F for "order" in ring_theory.localization and only found docs#is_localization.order_embedding

[Anne Baanen]

I don't think we have it: It didn't exist last time I touched localizations, and I don't think it got added after either.

[Apurva Nakade]

Would it be worth adding?
I need an order structure on Z localized away from 2. I can either prove it in full generality or just do the special case I need.

[Apurva Nakade]

I also ran into this: docs#normed_ring It might be easier to prove results about localization of normed_ring

[Anne Baanen]

If it helps your formalization, it's definitely worth adding!