mathlib3

025fe7cb - feat(group_theory/abelianization): An application of the three subgroups lemma (#12677)

feat(group_theory/abelianization): An application of the three subgroups lemma (#12677) This PR uses the three subgroups lemma to prove that `⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G`.