Partial derivatives' chain rule & product rule

Stream: Is there code for X?

[Shi Zhengyu]

As title suggests, is there code for partial derivatives' chain rule & product rule?

Thanks!

[Heather Macbeth]

@Shi Zhengyu In mathlib the differential calculus of several variables is phrased in terms of the Fréchet derivative. The chain rule is docs#has_fderiv_at.comp and the product rule is docs#has_fderiv_at.mul.

[Shi Zhengyu]

(deleted)