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>
