mathlib3

3ce710a7 - feat(group_theory/subsemigroup/membership): add membership criteria for subsemigroups (#13945)

feat(group_theory/subsemigroup/membership): add membership criteria for subsemigroups (#13945) This mimics the membership file for submoniods. However, because we have no `free_semigroup`, many features are missing from the corresponding submonid file. In particular, we have no notion of `subsemigroup.closure`. The reason for adding this now is so that we can develop some of the corresponding API for non-unital subsemirings. - [x] depends on: #13627