mathlib3

ee7bb12c - chore(ring_theory/ideal): Move ideal modules into a single folder (#3707)

chore(ring_theory/ideal): Move ideal modules into a single folder (#3707) The main motivation is to fix the odd inconsistency of `ideals` being plural, while most other files have singular names. Besides that, there seems to be precedent for grouping together such files