Theorem fderivWithin_const_smul_of_field

Modification history

2026-01-27 21:38
Mathlib/Analysis/Calculus/FDeriv/Add.lean
feat(Analysis/Calculus): generalize scalar multiplication actions (#34314) …
Deleted fderivWithin_const_smul_of_fieldView on Github →
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_fieldView on Github →