Discrete valuations

Stream: Is there code for X?

[Stepan Nesterov]

What is a good way to talk about a set of all finite places of a number field?
Mathlib has number fields in docs#number_theory.number_field, but doesn't seem to define places.
Mathematically, I would like to say that a place of a number field is a discrete valuation, but while mathlib does have docs#ring_theory.valuation.basic, and docs#ring_theory.discrete_valuation_ring, there doesn't seem to be a definition of a discrete valuation.

[Junyan Xu]

The current way to talk about finite places is to use docs#is_dedekind_domain.height_one_spectrum of the ring of integers; this is the spelling used to define S-integers (docs#set.integer), and you can also see how valuation_ring comes into the definition.

[Adam Topaz]

We do have the discrete valuation associated to a nonzero prime in a Dedekind domain

[Adam Topaz]

see https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/dedekind_domain/adic_valuation.lean