feat(group_theory/subgroup): Subgroup of subgroup is isomorphic to itself (#9204)
feat(group_theory/subgroup): Subgroup of subgroup is isomorphic to itself (#9204)

If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`.





leanprover-community/mathlib,leanprover-community/mathlib