mathlib3

d444a279 - feat(group_theory/transfer): Define the transfer homomorphism (#13446)

feat(group_theory/transfer): Define the transfer homomorphism (#13446) This PR adds a definition of the transfer homomorphism. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>