Theorem writtenInExtChartAt_sumInr_eventuallyEq_id

Modification history

2025-11-10 22:13
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
feat: mfderiv of Sum.inl and Sum.inr (#31200) …
Added writtenInExtChartAt_sumInr_eventuallyEq_idView on Github →