mathlib3

8f26acee - feat(group_theory/complement): transversal for the transfer homomorphism (#14182)

feat(group_theory/complement): transversal for the transfer homomorphism (#14182) In order to make use of the transfer homomorphism, there is a messy computation that must be done. This computation involves a specific choice of transversal, which is constructed in this PR. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>