Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-13 13:59 a9e7d333

View on Github →

chore(analysis/calculus/[f]deriv): generalize product formula to product in normed algebras (#9163)

Estimated changes

Modified src/analysis/calculus/deriv.lean

deleted theorem deriv_const_mul'

modified theorem deriv_const_mul

added theorem deriv_const_mul_field'

added theorem deriv_const_mul_field

deleted theorem deriv_mul_const'

modified theorem deriv_mul_const

added theorem deriv_mul_const_field'

added theorem deriv_mul_const_field

modified theorem has_deriv_at.const_mul

modified theorem has_deriv_at.mul_const

modified theorem has_deriv_within_at.const_mul

modified theorem has_deriv_within_at.mul_const

modified theorem has_strict_deriv_at.const_mul

modified theorem has_strict_deriv_at.mul_const

Modified src/analysis/calculus/fderiv.lean

modified theorem differentiable.const_mul

modified theorem differentiable.mul

modified theorem differentiable.mul_const

modified theorem differentiable_at.const_mul

modified theorem differentiable_at.mul

modified theorem differentiable_at.mul_const

modified theorem differentiable_on.const_mul

modified theorem differentiable_on.mul

modified theorem differentiable_on.mul_const

modified theorem fderiv_const_mul

added theorem fderiv_mul'

added theorem fderiv_mul_const'

modified theorem fderiv_mul_const

added theorem fderiv_within_mul'

added theorem fderiv_within_mul_const'

modified theorem has_fderiv_at.const_mul

added theorem has_fderiv_at.mul'

added theorem has_fderiv_at.mul_const'

modified theorem has_fderiv_at.mul_const

added theorem has_fderiv_within_at.mul'

added theorem has_fderiv_within_at.mul_const'

modified theorem has_fderiv_within_at.mul_const

modified theorem has_strict_fderiv_at.const_mul

added theorem has_strict_fderiv_at.mul'

added theorem has_strict_fderiv_at.mul_const'

modified theorem has_strict_fderiv_at.mul_const

Modified src/analysis/convex/specific_functions.lean

Modified src/analysis/special_functions/exp_log.lean

Modified src/analysis/special_functions/pow.lean