mathlib3

1b2d1a4a - feat(group_theory/sylow): Technical fusion lemma for Burnside's transfer theorem (#16800)

feat(group_theory/sylow): Technical fusion lemma for Burnside's transfer theorem (#16800) Burnside's transfer theorem requires a technical lemma obtained by applying Sylow's second theorem to the centralizer of an element. This technical lemmas states that if `P` is abelian, then `G`-conjugate elements of `P` are `N(P)`-conjugate. The fancy way of saying this is that "`N(P)` controls fusion in `P`.