Theorem differentiableAt_comp_const_add

Modification history

2025-10-06 22:06
Mathlib/Analysis/Calculus/Deriv/Add.lean
chore(Analysis/Calculus/Deriv): deprecate `differentiableAt_comp_const_add` (#28376)
Deleted differentiableAt_comp_const_addView on Github →
2024-08-15 17:24
Mathlib/Analysis/Calculus/Deriv/Add.lean
feat: Compute derivative of `fun x ↦ f (a - x)` (#15828) …
Added differentiableAt_comp_const_addView on Github →