mathlib3

1a2182cd - feat(group_theory/complement): Transversals as functions (#12732)

feat(group_theory/complement): Transversals as functions (#12732) This PR adds interpretations of transversals as functions mapping elements of `G` to the chosen coset representative.