Theorem MDifferentiableWithinAt.const_smul

Modification history

2026-05-16 15:19
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
feat: mfderivWithin_{add,neg,sub} (#39451) …
Added MDifferentiableWithinAt.const_smulView on Github →