Formal partial derivative

Stream: Is there code for X?

[Kenny Lau]

Formal partial derivative for mv_polynomial.
$\frac{\partial}{\partial x} (x^m y^n) = m x^{m-1} y^n$

[Kevin Buzzard]

@Shing Tak Lam formalised the definition for sure (in mathlib) -- it's pderiv in mv_polynomial.pderiv. There's pderiv_monomial_single and pderiv_eq_zero_of_not_mem_vars and pderiv_mul so that should do it.

[Kenny Lau]

docs#mv_polynomial.pderiv