feat(group_theory/subgroup/basic): `subgroup_of_self` (#9818)
feat(group_theory/subgroup/basic): `subgroup_of_self` (#9818)

A subgroup is the top subgroup of itself.





leanprover-community/mathlib,leanprover-community/mathlib