Abelianization

Stream: general

[Michael Howes]

@Kenny Lau I recently added the definition of the normal closure of a subset of a group to mathlib (see here: https://github.com/leanprover-community/mathlib/commit/d4343972661a252c53bd1ca1322a89448243c0f1).

With this definitions, I think I can make some of the definitions and proofs in group_theory\abelianization shorter. Would it be alright with you if I made these changes and put in a PR?

[Kenny Lau]

@Michael Howes Go ahead