Theorem IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt

Modification history

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