Theorem MDifferentiableWithinAt.add

Modification history

2026-03-05 11:23

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

chore(Geometry/Manifold/MFDeriv/SpecificFunctions): golf using custom… (#36009) …

Modified MDifferentiableWithinAt.add View on Github →

2025-07-03 21:54

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

feat: add missing API for MDifferentiable*.{add,neg} (#26702) …

Added MDifferentiableWithinAt.add View on Github →