Derivative_at_Maximum_or_Minimum
Provedcalculusderivativesextremaproofwiki
If f is differentiable at xi and has a local maximum or minimum there, then f'(xi) = 0.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue theorem Derivative_at_Maximum_or_Minimum (f : ℝ → ℝ) (ξ : ℝ) (hf : DifferentiableAt ℝ f ξ) (hmax : IsLocalMax f ξ ∨ IsLocalMin f ξ) : deriv f ξ = 0 := by sorry
Source