Commit 2025-12-31 18:19 7df6a0c2

View on Github →

feat: inner product of the gradient (#29877) Also, this PR enables the conj notation in the file.

Estimated changes

Modified Mathlib/Analysis/Calculus/Gradient/Basic.lean

modified theorem HasDerivAt.hasGradientAt

added theorem HasGradientAt.fderiv_apply

modified theorem HasGradientAt.hasDerivAt

added theorem HasGradientWithinAt.fderivWithin_apply

modified theorem gradient_eq_deriv

added theorem inner_gradientWithin_left

added theorem inner_gradientWithin_right

added theorem inner_gradient_left

added theorem inner_gradient_right