mathlib3
chore(data/fintype): change `unique.fintype` to priority 0
#1230

Merged

chore(data/fintype): change `unique.fintype` to priority 0 #1230

mergify merged 1 commit into master from ChrisHughes24-patch-1

chore(data/fintype): change `unique.fintype` to priority 0

61e10386

ChrisHughes24 requested a review 6 years ago

robertylewis approved these changes on 2019-07-15

robertylewis added ready-to-merge

mergify merged 46074fc1 into master 6 years ago

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

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone