Theorem differentiableWithinAt_smul_iff

Modification history

2025-07-07 08:46
Mathlib/Analysis/Calculus/FDeriv/Add.lean
feat: add version of fderiv_const_smul without differentiability hypotheses (#26700) …
Added differentiableWithinAt_smul_iffView on Github →