Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-27 07:06 89ece147

View on Github →

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.

Estimated changes