mathlib

6010cf52 - feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301)

feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301) This PR includes a few lemmas that prove certain Dedekind domains are PIDs. These will be useful for showing the ideal norm map is multiplicative. Co-Authored-By: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>