mathlib3
81618883 - feat(group_theory/subgroup): define normal bundled subgroups (#2947)

Commit

5 years ago

feat(group_theory/subgroup): define normal bundled subgroups (#2947) Most proofs are adapted from `deprecated/subgroup`.

Author

ChrisHughes24

Parents