Theorem mfderiv_sumInl

Modification history

2025-11-10 22:13

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

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

Added mfderiv_sumInl View on Github →