mathlib

4dec7b50 - feat(ring_theory/ideal): `(I : ideal R) • (⊤ : submodule R M)` (#12178)

feat(ring_theory/ideal): `(I : ideal R) • (⊤ : submodule R M)` (#12178) Two useful lemmas on the submodule spanned by `I`-scalar multiples. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>