partial derivatives guide

[lecopivo]

Added guide for partial derivatives based on my Zulip post #new members > partial derivative of a vector field @ 💬

[PatrickMassot]

Thanks Tomáš! I think this is useful but you should clearly say this guide is intended for downstream users, not further contributions to Mathlib, and explicitly point out that the Mathlib way is to replace EuclideanSpace ℝ (Fin n) with a real normed space (most often not even finite dimensional) and work with that instead.