Stream: Is there code for X?
Topic: Formal partial derivative
Kenny Lau (Oct 23 2020 at 08:48):
Formal partial derivative for
Kevin Buzzard (Oct 23 2020 at 09:14):
@Shing Tak Lam formalised the definition for sure (in mathlib) -- it's
pderiv_mul so that should do it.
Kenny Lau (Oct 23 2020 at 09:25):
Last updated: May 19 2021 at 03:22 UTC