Theorem MDifferentiableAt.smul

Modification history

2026-03-10 19:08
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
chore(Geometry/Manifold/MFDeriv/NormedSpace): use custom elaborators … (#36449) …
Modified MDifferentiableAt.smulView on Github →
2026-03-10 16:35
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: mfderiv_smul (#34263) …
Modified MDifferentiableAt.smulView on Github →
2024-11-28 15:29
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: manifold derivative of operations in vector spaces (#18849) …
Added MDifferentiableAt.smulView on Github →