# Commit 2020-09-10 08:56 49bb92dc

View on Github →feat(ring_theory/dedekind_domain): definitions (#4000)
Defines `is_dedekind_domain`

in three variants:

`is_dedekind_domain`

: Noetherian, Integrally closed, Krull dimension 1, thanks to @Vierkantor`is_dedekind_domain_dvr`

: Noetherian, localization at every nonzero prime is a DVR`is_dedekind_domain_inv`

: Every nonzero ideal is invertible. TODO: prove that these definitions are equivalent. This PR also includes some misc. lemmas required to show the definitions are independent of choice of fraction field. Co-Authored-By: mushokunosora knaka3435@gmail.com Co-Authored-By: faenuccio filippo.nuccio@univ-st-etienne.fr Co-Authored-By: Vierkantor vierkantor@vierkantor.com