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

Merged

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

mergify merged 2 commits into master from quot-map2

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

34ebfbea

jcommelin commented on 2019-10-05

rwbarton approved these changes on 2019-10-07

rwbarton added ready-to-merge

Merge branch 'master' into quot-map2

b2c2e61b

mergify merged ef7248f7 into master 6 years ago

mergify deleted the quot-map2 branch 6 years ago

Reviewers

rwbarton

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone