Commit 2022-03-16 10:05 bbc66b5e

feat(group_theory/subsemigroup/basic): subsemigroups (#12111) Port over submonoid implementation to a generalization: subsemigroups. Implement submonoids via extends using old_structure_cmd, since that is what subsemirings do. Copy over the attribution from submonoids because the content is almost unchanged. The submonoid file hasn't been changed, so no proofs rely on the subsemigroups proofs.