mathlib3

feat(data/quot): define `quotient.map₂'`, use it for group quotient

#1507

Merged