mathlib3

36e01301 - feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455) These lemmas generalize results that were originally in #15000. Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>