Commit 2026-11-10 17:26 4a6cf606

View on Github →

feat: isInvertible_fderivWithin_writtenInExtChartAt (#44843) If the mfderiv of f is injective (invertible), so is the fderivWithin of f written in extended charts.

Estimated changes