Commit 2024-04-06 08:38 74f9a89d

feat: add of_eq versions for lemmas on composition of derivatives (#11867) The versions we have assume that f is differentiable at h x and h is differentiable at x, to deduce that f o h is differentiable at x. In many applications, we have that f is differentiable at some point which happens to be equal to h x, but not definitionally, so one needs to jump through some hoops to apply the composition lemma. We add of_eq versions assuming instead that f is differentiable at y and that y = h x, which is much more flexible in practice.