Theorem IsDedekindDomain.isDedekindDomainDvr

Modification history

2024-09-24 17:42
Mathlib/RingTheory/DedekindDomain/Dvr.lean
feat(RingTheory/DedekindDomain): `IsDedekindDomainDvr` implies `IsDedekindDomain` (#16631) …
Deleted IsDedekindDomain.isDedekindDomainDvrView on Github →
2023-06-08 08:49
Mathlib/RingTheory/DedekindDomain/Dvr.lean
feat: port RingTheory.DedekindDomain.Dvr (#4846)
Added IsDedekindDomain.isDedekindDomainDvrView on Github →