Theorem HasGradientWithinAt.fderivWithin_apply

Modification history

2025-12-31 18:19
Mathlib/Analysis/Calculus/Gradient/Basic.lean
feat: inner product of the gradient (#29877) …
Added HasGradientWithinAt.fderivWithin_applyView on Github →