mathlib3

8914b68a - feat(ring_theory/dedekind_domain): ideals in a DD are cancellative (#8513)

feat(ring_theory/dedekind_domain): ideals in a DD are cancellative (#8513) This PR provides a `comm_cancel_monoid_with_zero` instance on integral ideals in a Dedekind domain. As a bonus, it deletes an out of date TODO comment. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>