Theorem isDedekindDomainDvr.of_formallyUnramified

Modification history

2026-08-10 10:19
Mathlib/RingTheory/Unramified/Dedekind.lean
chore: remove `IsDedekindDomainDvr` (#42367) …
Deleted isDedekindDomainDvr.of_formallyUnramifiedView on Github →
2026-03-26 08:33
Mathlib/RingTheory/Unramified/Dedekind.lean
feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) …
Added isDedekindDomainDvr.of_formallyUnramifiedView on Github →