Equivalent conditions for DVR #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
discrete_valuation_ring.tfae, we show that the following are equivalent for a
noetherian local domain
(R, m, k):
R is a discrete valuation ring
R is a valuation ring
R is a dedekind domain
R is integrally closed with a unique prime ideal
m is principal
dimₖ m/m² = 1
- Every nonzero ideal is a power of