Theorem MDifferentiableWithinAt.smul

Modification history

2026-03-10 16:35

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

feat: mfderiv_smul (#34263) …

Modified MDifferentiableWithinAt.smul View on Github →

2024-11-28 15:29

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

feat: manifold derivative of operations in vector spaces (#18849) …

Added MDifferentiableWithinAt.smul View on Github →