[Merged by Bors] - feat(ring_theory/non_unital_subsemiring/basic): introduce non-unital subsemirings and develop basic API

[j-loreaux]

• depends on: [Merged by Bors] - feat(group_theory/subsemigroup/{center, centralizer}): define center and centralizer as subsemigroups #13627
• depends on: [Merged by Bors] - fix(group_theory/subsemigroup/basic): change mul_one_class to has_mul #13747
• depends on: [Merged by Bors] - feat(ring_theory/submonoid/membership): generalize a few lemmas to mul_mem_class #13748
• depends on: [Merged by Bors] - feat(group_theory/subsemigroup/membership): add membership criteria for subsemigroups #13945
• depends on: [Merged by Bors] - feat(algebra/ring/{pi, prod, opposite}): add basic defs for non_unital_ring_hom #13958

---

[j-loreaux]

@eric-wieser: I requested your review specifically because I wrote all this up a few months ago and I noticed you had changed things recently with srestrict to take advantage of the new subobject type classes. I think I handled that correctly, but let me know if not.

[riccardobrasca]

LGTM. I think we can merge it and then maybe change something later if we have to.

[j-loreaux]

@eric-wieser, what do you think?

[ocfnash]

Thanks for doing this! I hope one day that we can delegate such code to the computer.

I left a few optional comments which I encourage you to consider but this is all OK as it stands.

bors d+

[bors]

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

Just in case: please merge master into this branch before sending it to bors.

[j-loreaux]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests