feat(group_theory): prove the 2nd isomorphism theorem for groups (#6187)
Define an `inclusion` homomorphism from a subgroup `H` contained in `K` to `K`. Add instance of `subgroup.normal` to `H ∩ N` in `H` whenever `N` is normal and use it to prove the 2nd isomorphism theorem for groups.
Co-authored-by: Adrián Doña Mateo <43966663+AdrianDoM@users.noreply.github.com>