mathlib3

0591c276 - feat(ring_theory/fractional_ideal): lemmas on `span_singleton _ x * I` (#8624)

feat(ring_theory/fractional_ideal): lemmas on `span_singleton _ x * I` (#8624) Useful in proving the basic properties of the ideal class group. See also #8622 which proves similar things for integral ideals.