refactor(deprecated/*): delete deprecated files

[kim-em]

If we'd prefer to leave these in place for old times sake, that's fine with me; this PR marks the milestone that they are no longer imported by the rest of mathlib!

---

• depends on: [Merged by Bors] - chore(group_theory/free_abelian_group): remove is_add_monoid_hom #13349
• depends on: [Merged by Bors] - refactor(control/fold): don't use is_monoid_hom #13350
• depends on: [Merged by Bors] - refactor(ring_theory/free_comm_ring): don't use is_ring_hom #13352
• depends on: [Merged by Bors] - chore(docs): don't use deprecated is_subring #13505

[jcommelin]

Thanks for decoupling mathlib from these files! I see that this PR is still doing some cleaning up, besides removing these files.

On the topic of removing deprecated/*: I think is_add_monoid_hom should not be a class. But it is a useful structure. And hence I would like to keep it around. So once mathlib is fully decoupled, I think we should do a refactors s/class/structure/, and then move these files out of deprecated/ and back into the main source tree.

[kim-em]

Hmm, this PR shouldn't be doing anything except deleting. Let me merge master again and see if it looks cleaner.

[kim-em]

Okay, I've added one more dependency, which cleans up some docs, and then this PR only deletes stuff. However, per the suggestion about is_add_monoid_hom, I will close this PR.

[kim-em]

I created a tracking issue at #13506. I have no intention of doing this. :-)

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - chore(group_theory/free_abelian_group): remove is_add_monoid_hom #13349
• [Merged by Bors] - refactor(control/fold): don't use is_monoid_hom #13350
• [Merged by Bors] - refactor(ring_theory/free_comm_ring): don't use is_ring_hom #13352
• [Merged by Bors] - chore(docs): don't use deprecated is_subring #13505
  By Dependent Issues (🤖). Happy coding!