Theorem mfderiv_sumInr

Modification history

2025-11-10 22:13

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

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

Added mfderiv_sumInr View on Github →