mathlib3

3de385a2 - feat(ring_theory/dedekind_domain): prime elements of `ideal A` are the prime ideals (#8718)

feat(ring_theory/dedekind_domain): prime elements of `ideal A` are the prime ideals (#8718) This shows that Dedekind domains have unique factorization into prime *ideals*, not just prime *elements* of the monoid `ideal A`. After some thinking, I believe Dedekind domains are the most common setting in which this equality hold. If anyone has a reference showing how to generalize this, that would be much appreciated.