mathlib
46074fc1
- chore(data/fintype): change `unique.fintype` to priority 0 (#1230)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
chore(data/fintype): change `unique.fintype` to priority 0 (#1230)
References
#1230 - chore(data/fintype): change `unique.fintype` to priority 0
Author
ChrisHughes24
Committer
mergify[bot]
Parents
0e9ac849
Loading