mathlib

ba6c84dd - feat(ring_theory/fractional_ideal): two span_singleton lemmas (#12656)