mathlib3
feat(data/finset): inj_on_of_surj_on_of_card_le
#1578

Merged

feat(data/finset): inj_on_of_surj_on_of_card_le #1578

mergify merged 5 commits into master from ChrisHughes24-patch-1

feat(data/finset): inj_on_of_surj_on_of_card_le

7ee15f99

jcommelin commented on 2019-10-21

Type ascriptions

5c2fa78d

function namespace

81180a68

kim-em approved these changes on 2019-10-21

kim-em added ready-to-merge

Merge branch 'master' into ChrisHughes24-patch-1

54adcaaa

Merge branch 'master' into ChrisHughes24-patch-1

cf679765

mergify merged 340178d8 into master 6 years ago

mergify deleted the ChrisHughes24-patch-1 branch 6 years ago

Reviewers

kim-em

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone