Commit 2023-05-28 22:16 f328e6f0

View on Github →

feat: port Analysis.Calculus.Deriv.Mul (#4440)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Deriv/Mul.lean

added theorem Differentiable.div_const

added theorem DifferentiableAt.div_const

added theorem DifferentiableOn.div_const

added theorem DifferentiableWithinAt.div_const

added theorem HasDerivAt.clm_apply

added theorem HasDerivAt.clm_comp

added theorem HasDerivAt.const_mul

added theorem HasDerivAt.div_const

added theorem HasDerivAt.mul

added theorem HasDerivAt.mul_const

added theorem HasDerivAt.smul

added theorem HasDerivAt.smul_const

added theorem HasDerivWithinAt.clm_apply

added theorem HasDerivWithinAt.clm_comp

added theorem HasDerivWithinAt.const_mul

added theorem HasDerivWithinAt.div_const

added theorem HasDerivWithinAt.mul

added theorem HasDerivWithinAt.mul_const

added theorem HasDerivWithinAt.smul

added theorem HasDerivWithinAt.smul_const

added theorem HasStrictDerivAt.clm_apply

added theorem HasStrictDerivAt.clm_comp

added theorem HasStrictDerivAt.const_mul

added theorem HasStrictDerivAt.div_const

added theorem HasStrictDerivAt.mul

added theorem HasStrictDerivAt.mul_const

added theorem HasStrictDerivAt.smul_const

added theorem derivWithin_clm_apply

added theorem derivWithin_clm_comp

added theorem derivWithin_const_mul

added theorem derivWithin_const_smul

added theorem derivWithin_div_const

added theorem derivWithin_mul

added theorem derivWithin_mul_const

added theorem derivWithin_smul

added theorem derivWithin_smul_const

added theorem deriv_clm_apply

added theorem deriv_clm_comp

added theorem deriv_const_mul

added theorem deriv_const_mul_field'

added theorem deriv_const_mul_field

added theorem deriv_const_smul

added theorem deriv_div_const

added theorem deriv_mul

added theorem deriv_mul_const

added theorem deriv_mul_const_field'

added theorem deriv_mul_const_field

added theorem deriv_smul

added theorem deriv_smul_const

added theorem hasDerivAt_mul_const