mathlib3

d3731988 - feat(group_theory/transfer): Prove Burnside's transfer theorem (#17263)

feat(group_theory/transfer): Prove Burnside's transfer theorem (#17263) This PR proves Burnside's transfer (or normal `p`-complement) theorem: If `hP : N(P) ≤ C(P)`, then `(transfer P hP).ker` is a normal `p`-complement.