ThmDex – An index of mathematical definitions, results, and conjectures.
Proof P3370 on R4909: Derivative for euclidean real self-dot product function
P3370
This result is a particular case of R4912: Strong derivative for symmetric euclidean real quadratic form where $A$ is an identity matrix. $\square$