Commit 2023-06-04 22:38 756d1f89

View on Github →

feat: port Analysis.Calculus.LagrangeMultipliers (#4663)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

added theorem IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt

added theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt

added theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d

added theorem IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt

added theorem IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt