Commit 2021-07-02 05:56 f5f8a20f

feat(analysis/calculus/fderiv_symmetric): prove that the second derivative is symmetric (#8104) We show that, if a function is differentiable over the reals around a point x, and is second-differentiable at x, then the second derivative is symmetric. In fact, we even prove a stronger statement for functions differentiable within a convex set, to be able to apply it for functions on the half-plane or the quadrant.