mathlib3

c30985dc - feat(group_theory/transfer): The transfer homomorphism `G →* center G` (#14520)

feat(group_theory/transfer): The transfer homomorphism `G →* center G` (#14520) This PR constructs the transfer homomorphism `G →* center G`. The bulk of this PR is a messy computation giving a criterion (`transfer_eq_pow`) for when the transfer homomorphism is the power map. The same criterion can be used to prove Burnside's transfer theorem.