Partial Derivative

Stream: general

[Henry Goodell]

I am relatively new here, but I have been doing some (admittedly very basic) work with LEAN, primarily formalizing very elementary proofs in complex analysis. It seems to me that there is no simple way to use about partial derivatives at the moment, am I incorrect (and if so what is this simple way)? And if I am not incorrect, is defining partial derivatives something that would be extraordinarily difficult, or just something that no one has gotten around to doing? Thank you in advance for your input.

[Johan Commelin]

This was discussed a while ago at #mathlib4 > Partial derivatives