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

These are, like #12178, split off from #12287






leanprover-community/mathlib,leanprover-community/mathlib