Commit 2022-05-02 15:58 64bc02c5

feat(ring_theory/dedekind_domain): Chinese remainder theorem for Dedekind domains (#13067) The general Chinese remainder theorem states R / I is isomorphic to a product of R / (P i ^ e i), where P i are comaximal, i.e. P i + P j = 1 for i ≠ j, and the infimum of all P i is I. In a Dedekind domain the theorem can be stated in a more friendly way, namely that the P i are the factors (in the sense of a unique factorization domain) of I. This PR provides two ways of doing so, and includes some more lemmas on the ideals in a Dedekind domain.