Theorem hasMFDerivWithinAt_inr

Modification history

2025-11-10 22:13

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

feat: mfderiv of Sum.inl and Sum.inr (#31200) …

Added hasMFDerivWithinAt_inr View on Github →