Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-04 06:59 c3d08357

View on Github →

chore(data/mv_polynomial): rename pderivative to pderiv (#4381) This name matches fderiv and deriv we have in analysis/.

Estimated changes

added theorem mv_polynomial.pderiv_C