Theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d

Modification history

2025-08-22 20:24
Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
refactor: Use `StrongDual` (#28726) …
Modified IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1dView on Github →
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 →