# mathlibdocumentation

ring_theory.dedekind_domain.dvr

# Dedekind domains #

This file defines an equivalent notion of a Dedekind domain (or Dedekind ring), namely a Noetherian integral domain where the localization at all nonzero prime ideals is a DVR (TODO: and shows that it is equivalent to the main definition).

## Main definitions #

• is_dedekind_domain_dvr alternatively defines a Dedekind domain as an integral domain that is Noetherian, and the localization at every nonzero prime ideal is a DVR.

## Implementation notes #

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. The ..._iff lemmas express this independence.

Often, definitions assume that Dedekind domains are not fields. We found it more practical to add a (h : ¬ is_field A) assumption whenever this is explicitly needed.

## Tags #

dedekind domain, dedekind ring

structure is_dedekind_domain_dvr (A : Type u_2) [comm_ring A] [is_domain A] :
Prop
• is_noetherian_ring :
• is_dvr_at_nonzero_prime : ∀ (P : ideal A), P ∀ (ᾰ : P.is_prime),

A Dedekind domain is an integral domain that is Noetherian, and the localization at every nonzero prime is a discrete valuation ring.

This is equivalent to is_dedekind_domain. TODO: prove the equivalence.