mathlib3

6979111c - 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.