Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 11:38 0c61fc46

View on Github →

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.

Estimated changes