mathlib3

a8406c25 - feat(ring_theory/ideals): Do not define ideals in terms of submodules