mathlib3
feat(logic/basic): a few lemmas about `exists_unique`
#2283

Merged

feat(logic/basic): a few lemmas about `exists_unique` #2283

mergify merged 4 commits into master from exists_unique

feat(logic/basic): a few lemmas about `exists_unique`

ab48a152

bryangingechen added awaiting-review

jcommelin approved these changes on 2020-03-30

ChrisHughes24 requested changes on 2020-03-31

ChrisHughes24 added awaiting-author

ChrisHughes24 removed awaiting-review

Merge branch 'master' into exists_unique

0ea12720

Use dependent types as suggested by Chris Hughes

02baca2a

urkud removed awaiting-author

urkud added awaiting-review

jcommelin requested a review from

ChrisHughes24 6 years ago

ChrisHughes24 approved these changes on 2020-04-02

ChrisHughes24 removed awaiting-review

ChrisHughes24 added ready-to-merge

Merge branch 'master' into exists_unique

84a2411b

mergify merged 654533ff into master 6 years ago

mergify deleted the exists_unique branch 6 years ago

Reviewers

ChrisHughes24

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone