Theorem differentiableAt_comp_neg_iff

Modification history

2024-08-15 17:24
Mathlib/Analysis/Calculus/Deriv/Add.lean
feat: Compute derivative of `fun x ↦ f (a - x)` (#15828) …
Deleted differentiableAt_comp_neg_iffView on Github →
2024-03-06 11:04
Mathlib/Analysis/Calculus/Deriv/Add.lean
feat(Analysis/Calculus/{Iterated}Deriv/*): add lemmas on composition with negation (#11173) …
Added differentiableAt_comp_neg_iffView on Github →