Commit 2022-07-02 14:14 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) In this PR, we show that given Dedekind domains R and S with ideals I and Jrespectively, 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 as a corollary of this statement. For previous discussion concerning the structure of this PR and the results it proves, see #9345