Theorem HasGradientAt.fderiv_apply

Modification history

2026-10-15 10:19
Mathlib/Analysis/Calculus/Gradient/Basic.lean
chore: protect various declarations related to (f)derivs (#44875) …
Deleted HasGradientAt.fderiv_applyView on Github →
2025-12-31 18:19
Mathlib/Analysis/Calculus/Gradient/Basic.lean
feat: inner product of the gradient (#29877) …
Added HasGradientAt.fderiv_applyView on Github →