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