Theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt

Modification history

2023-08-10 19:52
Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAtView on Github →
2023-06-04 22:38
Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
feat: port Analysis.Calculus.LagrangeMultipliers (#4663)
Added IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAtView on Github →