mathlib3

530b948f - chore(ring_theory/dedekind_domain): better, computable, defeq in `cancel_comm_monoid_with_zero` instance (#15752)

chore(ring_theory/dedekind_domain): better, computable, defeq in `cancel_comm_monoid_with_zero` instance (#15752) The `ideal.cancel_comm_monoid_with_zero` instance transports the cancellativity property across the injection from `ideal` into `fractional_ideal`. However, it also transported all the operations on ideals, making the instance `noncomputable`. We can just use the `ideal.semiring` instance for all these operations so the instance becomes computable again. In addition, this results in better defeq as we don't have to unfold through `fractional_ideal` to get to multiplication.