feat(group_theory/bundled_subgroup): bundled subgroup (#2140) · leanprover-community/mathlib@5e2025f · GitHub

Commit

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

Browse files

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>

Loading branch information

3 people committed Apr 22, 2020

1 parent 585d77a commit 5e2025f