Commit 2020-09-09 16:00 11e62b0b
View on Github →fix(data/mv_polynomial/pderivative): rename variables and file, make it universe polymorphic (#4083)
This file originally used different variable names to the rest of mv_polynomial
. I've changed it to now use the same conventions as the other files.
I also renamed the file to pderivative.lean
to be consistent with derivative.lean
for polynomials.
The types of the coefficient ring and the indexing variables are now universe polymorphic.
The diff shows it as new files, but the only changes are fixing the statements and proofs.