Theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d

Modification history

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