Theorem IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt

Modification history

2023-06-04 22:38
Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
feat: port Analysis.Calculus.LagrangeMultipliers (#4663)
Added IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAtView on Github →