[Merged by Bors] - chore(ring_theory/ideals): Move the definition of ideals out of algebra/module

[eric-wieser]

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.

---

[Vierkantor]

Ring theory does seem like a more appropriate place. Is there a reason for this change apart from neatness (e.g. better compilation times)?

[eric-wieser]

Is there a reason for this change apart from neatness (e.g. better compilation times)?

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.

As a follow-up, I wonder if (again for the sake of neatness), the following renames should happen in some future PR:

• ideals.lean → ideal/basic.lean
• ideal_over.lean → ideal/over.lean
• ideal_operations.lean → ideal/operations.lean

[Vierkantor]

Could you fix the broken build? It looks like the implicit variables are being declared in a different order for mul_mem_right ({a b : α} now comes before [comm_ring α]; my intuition says the old way is better).

[eric-wieser]

my intuition says the old way is better

Unfortunately, there are two old ways here. To avoid having to change every caller of these theorems, I've tried to leave all the lemmas with the same argument order they have before. At some point, someone should probably make them use the same argument order, but that feels out of scope for this PR.

[Vierkantor]

Thanks 🎉

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests