mathlib

926daa81 - feat(ring_theory/dedekind_domain): localizing a Dedekind domain at a prime gives DVR (#18264)

feat(ring_theory/dedekind_domain): localizing a Dedekind domain at a prime gives DVR (#18264) This PR shows one direction of the implication `is_dedekind_domain → is_dedekind_domain_dvr`. The first step is to show that any localization of a Dedekind domain is again Dedekind, then use the very useful `discrete_valuation_ring.tfae` to show that this implies the localization at a prime is a DVR. Beyond general usefulness, I need this for `ideal.span_norm`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>