mathlib3

50088c97 - feat(ring_theory/dedekind_domain/ideal): add more span_singleton lemmas (#18047)