Theorem ContinuousLinearMap.derivWithin_of_bilinear

Modification history

2025-01-19 11:52
Mathlib/Analysis/Calculus/Deriv/Mul.lean
feat: remove `UniqueDiffWithinAt` assumptions for one-dimensional derivative (#20816) …
Modified ContinuousLinearMap.derivWithin_of_bilinearView on Github →
2024-04-05 06:15
Mathlib/Analysis/Calculus/Deriv/Mul.lean
feat: `deriv` versions of composition lemmas with bilinear maps (#11868) …
Added ContinuousLinearMap.derivWithin_of_bilinearView on Github →