feat(group_theory/transfer): The kernel of the transfer homomorphism `G →* P` is disjoint from every `p`-group (#16914)
feat(group_theory/transfer): The kernel of the transfer homomorphism `G →* P` is disjoint from every `p`-group (#16914)

This PR proves if `P` is a Sylow `p`-subgroup of `G`, then the kernel of the transfer homomorphism `G →* P` is disjoint from every `p`-group. This is getting very close to Burnside's transfer theorem. I also added variables lines for some typeclass assumptions.





leanprover-community/mathlib,leanprover-community/mathlib