mathlib
89ece147
- fix(data/mv_polynomial): generalize equivs to comm_semiring (#1621)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
fix(data/mv_polynomial): generalize equivs to comm_semiring (#1621) This apparently makes the elaborator's job a lot easier, and reduces the compile time of the whole module by a factor of 3.
References
#1621 - fix(data/mv_polynomial): generalize equivs to comm_semiring
Author
rwbarton
Committer
mergify[bot]
Parents
8a45d98f
Loading