mathlib
c9fc9bf7
- refactor(order/filter/pointwise): Cleanup (#12789)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
refactor(order/filter/pointwise): Cleanup (#12789) * Reduce typeclass assumptions from `monoid` to `has_mul` * Turn lemmas into instances * Use hom classes rather than concrete hom types * Golf
Author
YaelDillies
Parents
2b6b9ffc
Loading