mathlib3

0672fa47 - feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID (#15758)

feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID (#15758) A definition plus some extra lemmas about PIDs that will be used in #15000 Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>