mathlib

9deac65c - feat(ring_theory/ideal): more lemmas on ideals multiplied with submodules (#12401)