Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-28 22:54 1e45472a

View on Github →

feat(analysis/calculus): Lagrange multipliers (#6431)

Estimated changes

Modified src/algebra/module/linear_map.lean

modified theorem linear_map.to_add_monoid_hom_coe

Created src/analysis/calculus/lagrange_multipliers.lean

added theorem is_local_extr_on.exists_linear_map_of_has_strict_fderiv_at

added theorem is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at

added theorem is_local_extr_on.linear_dependent_of_has_strict_fderiv_at

added theorem is_local_extr_on.range_ne_top_of_has_strict_fderiv_at

Modified src/data/fintype/card.lean

added theorem fintype.prod_option

Modified src/linear_algebra/basic.lean

Modified src/linear_algebra/pi.lean

added def linear_equiv.pi_ring

added theorem linear_equiv.pi_ring_apply

added theorem linear_equiv.pi_ring_symm_apply

Modified src/order/filter/extr.lean

added theorem is_max_filter.tendsto_principal_Iic

added theorem is_min_filter.tendsto_principal_Ici

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.coe_sum'

added theorem continuous_linear_map.coe_sum

Modified src/topology/continuous_on.lean