mathlib3

9e701b98 - feat(ring_theory/dedekind_domain): If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape (#11053)

feat(ring_theory/dedekind_domain): If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape (#11053) In this PR, we show that given Dedekind domains `R` and `S` with ideals `I` and `J`respectively, if quotients `R/I` and `S/J` are isomorphic, then the prime factorizations of `I` and `J` have the same shape, i.e. they have the same number of prime factors and up to permutation these prime factors have the same multiplicities. We can then get [the Dedekind-Kummer theorem](https://kconrad.math.uconn.edu/blurbs/gradnumthy/dedekindf.pdf) as a corollary of this statement. For previous discussion concerning the structure of this PR and the results it proves, see #9345 Co-authored-by: Anne Baanen. Co-authored-by: Johan Commelin <johan@commelin.net>