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.





leanprover-community/mathlib,leanprover-community/mathlib