mathlib3
feat(data/finset): monotone bijection from fin k
#2163

Merged

feat(data/finset): monotone bijection from fin k #2163

mergify merged 8 commits into master from sgouezel_fin

feat(data/finset): increasing bijection between fin k and an ordered …

8f835c85

fix build

0e6b19c8

fix linter

972bb956

urkud commented on 2020-03-15

make argument explicit

5f87becf

jcommelin commented on 2020-03-16

add equiv for fintype

06b534d9

sgouezel added awaiting-review

cipher1024 assigned

jcommelin 5 years ago

jcommelin changed the title ~~feat(data/finset): increasing bijection from fin k.~~ feat(data/finset): monotone bijection from fin k 5 years ago

jcommelin removed awaiting-review

jcommelin added awaiting-author

merge master

39dc522d

sgouezel removed awaiting-author

sgouezel added awaiting-review

jcommelin removed awaiting-review

jcommelin added ready-to-merge

jcommelin approved these changes on 2020-03-19

Merge branch 'master' into sgouezel_fin

eebbd743

Merge branch 'master' into sgouezel_fin

ab32ab4c

mergify merged 344a41e8 into master 5 years ago

mergify deleted the sgouezel_fin branch 5 years ago

Reviewers

jcommelin

urkud

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone