Theorem inner_gradientWithin_left

Modification history

2026-06-01 21:42
Mathlib/Analysis/Calculus/Gradient/Basic.lean
refactor(Analysis/Calculus/Gradient): ungate `inner_gradient` lemmas (#39203) …
Modified inner_gradientWithin_leftView on Github →
2025-12-31 18:19
Mathlib/Analysis/Calculus/Gradient/Basic.lean
feat: inner product of the gradient (#29877) …
Added inner_gradientWithin_leftView on Github →