mathlib
6b4e2691
- chore(data/fintype/basic): rename some instances (#11845)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(data/fintype/basic): rename some instances (#11845) Rename instances from `infinite.multiset.infinite` etc to `multiset.infinite` etc; rename `infinite.set.infinite` to `infinite.set` to avoid name clash. Also add `option.infinite`.
Author
urkud
Parents
b0d9761b
Loading