Zulip Chat Archive

Stream: Is there code for X?

Topic: Formal partial derivative


view this post on Zulip Kenny Lau (Oct 23 2020 at 08:48):

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

view this post on Zulip Kevin Buzzard (Oct 23 2020 at 09:14):

@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.

view this post on Zulip Kenny Lau (Oct 23 2020 at 09:25):

docs#mv_polynomial.pderiv


Last updated: May 19 2021 at 03:22 UTC