mathlib3

253712e1 - feat(ring_theory/ideal): lemmas on `ideal.span {x} * I` (#8622)

feat(ring_theory/ideal): lemmas on `ideal.span {x} * I` (#8622) Originally created for being used in the context of the ideal class group, but didn't end up being used. Hopefully they are still useful for others.