mathlib3

64bc02c5 - feat(ring_theory/dedekind_domain): Chinese remainder theorem for Dedekind domains (#13067)

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.