mathlib3

1e05171a - feat(ring_theory/dedekind_domain/ideal): add fractional_ideal.coe_ideal_span_singleton mul_inv and inv_mul lemmas (#18032)