mathlib3

cf43320e - feat(group_theory/transfer): Homomorphism for Burnside's transfer theorem (#16818)

feat(group_theory/transfer): Homomorphism for Burnside's transfer theorem (#16818) This PR constructs the homomorphism `G →* P` for Burnside's transfer theorem and proves that it is the `[G : P]`th power map on elements of `P`. Burnside's transfer theorem will follow reasonably quickly from this (the homomorphism is an isomorphism on `P`, so the kernel is disjoint from `P`, so the kernel is disjoint from every Sylow by normality, so the kernel cannot have order divisible by p, so the homomorphism is surjective and the kernel is a normal p-complement).