Commit 2024-09-24 17:42 6d063869
View on Github →feat(RingTheory/DedekindDomain): IsDedekindDomainDvr implies IsDedekindDomain (#16631)
Prove that IsDedekindDomainDvr implies IsDedekindDomain, i.e., if an integral domain is Noetherian, and the localization at every nonzero prime is a discrete valuation ring, then it is a Dedekind domain.
- depends on: #16558