Partial derivatives commute

Stream: Is there code for X?

[Geoffrey Irving]

What results do we have about partial derivatives commuting? I can't find them, but it seems unlikely that they don't exist.

[Yaël Dillies]

It's discussed at length in #mathlib4 > Partial derivatives

[Sébastien Gouëzel]

See docs#second_derivative_symmetric_of_eventually

[Sébastien Gouëzel]

I have more results and an expanded API in a branch, see for instance https://github.com/leanprover-community/mathlib4/blob/SG_lie/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean

[Geoffrey Irving]

Neat, thank you!