Commit 2020-09-10 08:56 49bb92dc

View on Github →

feat(ring_theory/dedekind_domain): definitions (#4000) Defines is_dedekind_domain in three variants:

  1. is_dedekind_domain: Noetherian, Integrally closed, Krull dimension 1, thanks to @Vierkantor
  2. is_dedekind_domain_dvr: Noetherian, localization at every nonzero prime is a DVR
  3. 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 Co-Authored-By: faenuccio Co-Authored-By: Vierkantor

Estimated changes