mathlib

c63dad10 - chore(ring_theory/ideals): Move the definition of ideals out of algebra/module (#3692)

chore(ring_theory/ideals): Move the definition of ideals out of algebra/module (#3692) Neatness was the main motivation - it makes it easier to reason about what would need doing in #3635. It also results in somewhere sensible for the docs about ideals. Also adds a very minimal docstring to `ring_theory/ideals.lean`.