Commit 2025-11-10 22:13 cd3a2eba

View on Github →

feat: mfderiv of Sum.inl and Sum.inr (#31200) This will be used for #31351 in the bordism theory project.

Estimated changes

added theorem hasMFDerivAt_inl
added theorem hasMFDerivAt_inr
added theorem hasMFDerivWithinAt_inl
added theorem hasMFDerivWithinAt_inr
added theorem mfderivWithin_sumInl
added theorem mfderivWithin_sumInr
added theorem mfderiv_sumInl
added theorem mfderiv_sumInr