Commit 2020-08-05 11:37 c63dad10
View on Github →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.