Commit 2023-12-08 10:23 cf7d718e

feat: invariance of the derivative under translation (#8614) This adds a new file Mathlib.Analysis.Calculus.Deriv.Shift that contains two lemmas

lemma HasDerivAt.comp_const_add {𝕜 : Type*} [NontriviallyNormedField 𝕜] (a x : 𝕜) {𝕜' : Type*}
    [NormedAddCommGroup 𝕜'] [NormedSpace 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (a + x)) :
    HasDerivAt (fun x ↦ h (a + x)) h' x := ...
lemma HasDerivAt.comp_add_const {𝕜 : Type*} [NontriviallyNormedField 𝕜] (x a : 𝕜) {𝕜' : Type*}
    [NormedAddCommGroup 𝕜'] [NormedSpace 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h' : 𝕜'}
    (hh : HasDerivAt h h' (x + a)) :
    HasDerivAt (fun x ↦ h (x + a)) h' x  := ...