Commit 2023-09-09 11:57 54527c58

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.