Theorem fderivWithin_const_smul_of_invertible

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 fderivWithin_const_smul_of_invertibleView on Github →