Commit 2023-05-25 11:48 5e909893

View on Github →

feat: port Analysis.Calculus.FDeriv.Mul (#4241)

Estimated changes

Modified Mathlib.lean

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

added theorem Differentiable.clm_apply

added theorem Differentiable.clm_comp

added theorem Differentiable.const_mul

added theorem Differentiable.mul

added theorem Differentiable.mul_const

added theorem Differentiable.pow

added theorem Differentiable.smul

added theorem Differentiable.smul_const

added theorem DifferentiableAt.clm_apply

added theorem DifferentiableAt.clm_comp

added theorem DifferentiableAt.const_mul

added theorem DifferentiableAt.mul

added theorem DifferentiableAt.mul_const

added theorem DifferentiableAt.pow

added theorem DifferentiableAt.smul

added theorem DifferentiableAt.smul_const

added theorem DifferentiableOn.clm_apply

added theorem DifferentiableOn.clm_comp

added theorem DifferentiableOn.const_mul

added theorem DifferentiableOn.mul

added theorem DifferentiableOn.mul_const

added theorem DifferentiableOn.pow

added theorem DifferentiableOn.smul

added theorem DifferentiableOn.smul_const

added theorem DifferentiableWithinAt.clm_apply

added theorem DifferentiableWithinAt.clm_comp

added theorem DifferentiableWithinAt.const_mul

added theorem DifferentiableWithinAt.mul

added theorem DifferentiableWithinAt.mul_const

added theorem DifferentiableWithinAt.pow

added theorem DifferentiableWithinAt.smul

added theorem DifferentiableWithinAt.smul_const

added theorem HasFDerivAt.clm_apply

added theorem HasFDerivAt.clm_comp

added theorem HasFDerivAt.const_mul

added theorem HasFDerivAt.mul'

added theorem HasFDerivAt.mul

added theorem HasFDerivAt.mul_const'

added theorem HasFDerivAt.mul_const

added theorem HasFDerivAt.smul

added theorem HasFDerivAt.smul_const

added theorem HasFDerivWithinAt.clm_apply

added theorem HasFDerivWithinAt.clm_comp

added theorem HasFDerivWithinAt.const_mul

added theorem HasFDerivWithinAt.mul'

added theorem HasFDerivWithinAt.mul

added theorem HasFDerivWithinAt.mul_const'

added theorem HasFDerivWithinAt.mul_const

added theorem HasFDerivWithinAt.smul

added theorem HasFDerivWithinAt.smul_const

added theorem HasStrictFDerivAt.clm_apply

added theorem HasStrictFDerivAt.clm_comp

added theorem HasStrictFDerivAt.const_mul

added theorem HasStrictFDerivAt.mul'

added theorem HasStrictFDerivAt.mul

added theorem HasStrictFDerivAt.mul_const'

added theorem HasStrictFDerivAt.mul_const

added theorem HasStrictFDerivAt.smul

added theorem HasStrictFDerivAt.smul_const

added theorem differentiableAt_inverse

added theorem fderivWithin_clm_apply

added theorem fderivWithin_clm_comp

added theorem fderivWithin_const_mul

added theorem fderivWithin_mul'

added theorem fderivWithin_mul

added theorem fderivWithin_mul_const'

added theorem fderivWithin_mul_const

added theorem fderivWithin_smul

added theorem fderivWithin_smul_const

added theorem fderiv_clm_apply

added theorem fderiv_clm_comp

added theorem fderiv_const_mul

added theorem fderiv_inverse

added theorem fderiv_mul'

added theorem fderiv_mul

added theorem fderiv_mul_const'

added theorem fderiv_mul_const

added theorem fderiv_smul

added theorem fderiv_smul_const

added theorem hasFDerivAt_ring_inverse