mathlib3
f8c303ea
- refactor(order/filter/pointwise): Localize instances (#13898)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
refactor(order/filter/pointwise): Localize instances (#13898) Localize pointwise `filter` instances into the `pointwise` locale, as is done for `set` and `finset`.
Author
YaelDillies
Parents
627f81b4
Loading