feat(group_theory/bundled_subgroup): bundled subgroup (#2140)

Add bundled subgroups. While `is_subgroup` is a class taking `s : set G` as an argument, `subgroup G` is a structure with a field `carrier : set G` and a coercion to `set G`.



Co-authored-by: JasonKYi <57107612+JasonKYi@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: kex-y