feat: derivative along a vector (#7038)

Prerequisite for Rademacher's theorem in #7003

We currently have in mathlib the Fréchet derivative, and the derivative of maps defined on the scalar field. In this PR, we introduce another notion, the derivative along a line. It is more elementary (but less well behaved) than the full Fréchet derivative.

The API is essentially copied from the file on the one-dimensional derivative, with a few additions that have proved useful for Rademacher's theorem. The API could definitely be expanded, but it's already heavy... I have put everything in the single file `LineDeriv/Basic.lean`, mimicking the directory structure for `FDeriv` and `Deriv` and leaving open the possibility to add other files in this folder with more API.

Author: sgouezel

Mathlib.lean

@@ -588,6 +588,7 @@ import Mathlib.Analysis.Calculus.Inverse
 import Mathlib.Analysis.Calculus.IteratedDeriv
 import Mathlib.Analysis.Calculus.LHopital
 import Mathlib.Analysis.Calculus.LagrangeMultipliers
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
 import Mathlib.Analysis.Calculus.LocalExtr.Basic
 import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
 import Mathlib.Analysis.Calculus.LocalExtr.Rolle