chore(group_theory/submonoid): split into 3 files (#3058)
Now
* `group_theory.submonoid.basic` contains the definition, `complete_lattice` structure, and some basic facts about `closure`;
* `group_theory.submonoid.operations` contains definitions of various operations on submonoids;
* `group_theory.submonoid.membership` contains various facts about membership in a submonoid or the submonoid closure of a set.
