basic): equiv.nonempty_iff_nonempty
#1020

Merged

feat(data/equiv/basic): equiv.nonempty_iff_nonempty #1020

mergify merged 2 commits into master from rwbarton-equiv-nonempty

feat(data/equiv/basic): equiv.nonempty_iff_nonempty

4a823ecf

rwbarton requested a review 7 years ago

robertylewis dismissed these changes on 2019-05-13

robertylewis added ready-to-merge

Merge branch 'master' into rwbarton-equiv-nonempty

c413a8c0

jcommelin approved these changes on 2019-05-13

mergify dismissed their stale review 7 years ago

Pull request has been modified.

mergify merged f8385b19 into master 7 years ago

mergify deleted the rwbarton-equiv-nonempty branch 7 years ago

Reviewers

jcommelin

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone