mathlib

c3442db1 - chore(ring_theory/dedekind_domain/ideal): remove fractional_ideal in open namespaces (#18033)