mathlib documentation

ring_theory.valuation.tfae

Equivalent conditions for DVR #

In discrete_valuation_ring.tfae, we show that the following are equivalent for a noetherian local domain (R, m, k):