Commit 2023-06-05 00:03 716d796e

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Deriv (#4653)

Estimated changes

added theorem Complex.contDiff_cos
added theorem Complex.contDiff_cosh
added theorem Complex.contDiff_sin
added theorem Complex.contDiff_sinh
added theorem Complex.deriv_cos'
added theorem Complex.deriv_cos
added theorem Complex.deriv_cosh
added theorem Complex.deriv_sin
added theorem Complex.deriv_sinh
added theorem Complex.hasDerivAt_cos
added theorem Complex.hasDerivAt_sin
added theorem ContDiff.ccos
added theorem ContDiff.ccosh
added theorem ContDiff.cos
added theorem ContDiff.cosh
added theorem ContDiff.csin
added theorem ContDiff.csinh
added theorem ContDiff.sin
added theorem ContDiff.sinh
added theorem ContDiffAt.ccos
added theorem ContDiffAt.ccosh
added theorem ContDiffAt.cos
added theorem ContDiffAt.cosh
added theorem ContDiffAt.csin
added theorem ContDiffAt.csinh
added theorem ContDiffAt.sin
added theorem ContDiffAt.sinh
added theorem ContDiffOn.ccos
added theorem ContDiffOn.ccosh
added theorem ContDiffOn.cos
added theorem ContDiffOn.cosh
added theorem ContDiffOn.csin
added theorem ContDiffOn.csinh
added theorem ContDiffOn.sin
added theorem ContDiffOn.sinh
added theorem ContDiffWithinAt.ccos
added theorem ContDiffWithinAt.ccosh
added theorem ContDiffWithinAt.cos
added theorem ContDiffWithinAt.cosh
added theorem ContDiffWithinAt.csin
added theorem ContDiffWithinAt.csinh
added theorem ContDiffWithinAt.sin
added theorem ContDiffWithinAt.sinh
added theorem Differentiable.ccos
added theorem Differentiable.ccosh
added theorem Differentiable.cos
added theorem Differentiable.cosh
added theorem Differentiable.csin
added theorem Differentiable.csinh
added theorem Differentiable.sin
added theorem Differentiable.sinh
added theorem DifferentiableAt.ccos
added theorem DifferentiableAt.ccosh
added theorem DifferentiableAt.cos
added theorem DifferentiableAt.cosh
added theorem DifferentiableAt.csin
added theorem DifferentiableAt.csinh
added theorem DifferentiableAt.sin
added theorem DifferentiableAt.sinh
added theorem DifferentiableOn.ccos
added theorem DifferentiableOn.ccosh
added theorem DifferentiableOn.cos
added theorem DifferentiableOn.cosh
added theorem DifferentiableOn.csin
added theorem DifferentiableOn.csinh
added theorem DifferentiableOn.sin
added theorem DifferentiableOn.sinh
added theorem HasDerivAt.ccos
added theorem HasDerivAt.ccosh
added theorem HasDerivAt.cos
added theorem HasDerivAt.cosh
added theorem HasDerivAt.csin
added theorem HasDerivAt.csinh
added theorem HasDerivAt.sin
added theorem HasDerivAt.sinh
added theorem HasDerivWithinAt.ccos
added theorem HasDerivWithinAt.ccosh
added theorem HasDerivWithinAt.cos
added theorem HasDerivWithinAt.cosh
added theorem HasDerivWithinAt.csin
added theorem HasDerivWithinAt.csinh
added theorem HasDerivWithinAt.sin
added theorem HasDerivWithinAt.sinh
added theorem HasFDerivAt.ccos
added theorem HasFDerivAt.ccosh
added theorem HasFDerivAt.cos
added theorem HasFDerivAt.cosh
added theorem HasFDerivAt.csin
added theorem HasFDerivAt.csinh
added theorem HasFDerivAt.sin
added theorem HasFDerivAt.sinh
added theorem HasFDerivWithinAt.ccos
added theorem HasFDerivWithinAt.cos
added theorem HasFDerivWithinAt.cosh
added theorem HasFDerivWithinAt.csin
added theorem HasFDerivWithinAt.sin
added theorem HasFDerivWithinAt.sinh
added theorem HasStrictDerivAt.ccos
added theorem HasStrictDerivAt.ccosh
added theorem HasStrictDerivAt.cos
added theorem HasStrictDerivAt.cosh
added theorem HasStrictDerivAt.csin
added theorem HasStrictDerivAt.csinh
added theorem HasStrictDerivAt.sin
added theorem HasStrictDerivAt.sinh
added theorem HasStrictFDerivAt.ccos
added theorem HasStrictFDerivAt.cos
added theorem HasStrictFDerivAt.cosh
added theorem HasStrictFDerivAt.csin
added theorem HasStrictFDerivAt.sin
added theorem HasStrictFDerivAt.sinh
added theorem Real.abs_sinh
added theorem Real.contDiff_cos
added theorem Real.contDiff_cosh
added theorem Real.contDiff_sin
added theorem Real.contDiff_sinh
added theorem Real.cosh_le_cosh
added theorem Real.cosh_lt_cosh
added theorem Real.cosh_strictMonoOn
added theorem Real.deriv_cos'
added theorem Real.deriv_cos
added theorem Real.deriv_cosh
added theorem Real.deriv_sin
added theorem Real.deriv_sinh
added theorem Real.hasDerivAt_cos
added theorem Real.hasDerivAt_cosh
added theorem Real.hasDerivAt_sin
added theorem Real.hasDerivAt_sinh
added theorem Real.one_le_cosh
added theorem Real.one_lt_cosh
added theorem Real.self_le_sinh_iff
added theorem Real.self_lt_sinh_iff
added theorem Real.sinh_inj
added theorem Real.sinh_injective
added theorem Real.sinh_le_self_iff
added theorem Real.sinh_le_sinh
added theorem Real.sinh_lt_self_iff
added theorem Real.sinh_lt_sinh
added theorem Real.sinh_neg_iff
added theorem Real.sinh_nonneg_iff
added theorem Real.sinh_nonpos_iff
added theorem Real.sinh_pos_iff
added theorem Real.sinh_strictMono
added theorem derivWithin_ccos
added theorem derivWithin_ccosh
added theorem derivWithin_cos
added theorem derivWithin_cosh
added theorem derivWithin_csin
added theorem derivWithin_csinh
added theorem derivWithin_sin
added theorem derivWithin_sinh
added theorem deriv_ccos
added theorem deriv_ccosh
added theorem deriv_cos
added theorem deriv_cosh
added theorem deriv_csin
added theorem deriv_csinh
added theorem deriv_sin
added theorem deriv_sinh
added theorem fderivWithin_ccos
added theorem fderivWithin_ccosh
added theorem fderivWithin_cos
added theorem fderivWithin_cosh
added theorem fderivWithin_csin
added theorem fderivWithin_csinh
added theorem fderivWithin_sin
added theorem fderivWithin_sinh
added theorem fderiv_ccos
added theorem fderiv_ccosh
added theorem fderiv_cos
added theorem fderiv_cosh
added theorem fderiv_csin
added theorem fderiv_csinh
added theorem fderiv_sin
added theorem fderiv_sinh