Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-05 00:03
716d796e
View on Github →
feat: port Analysis.SpecialFunctions.Trigonometric.Deriv (
#4653
)
depends on:
#4651
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
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.differentiableAt_cos
added
theorem
Complex.differentiableAt_cosh
added
theorem
Complex.differentiableAt_sin
added
theorem
Complex.differentiableAt_sinh
added
theorem
Complex.differentiable_cos
added
theorem
Complex.differentiable_cosh
added
theorem
Complex.differentiable_sin
added
theorem
Complex.differentiable_sinh
added
theorem
Complex.hasDerivAt_cos
added
theorem
Complex.hasDerivAt_cosh
added
theorem
Complex.hasDerivAt_sin
added
theorem
Complex.hasDerivAt_sinh
added
theorem
Complex.hasStrictDerivAt_cos
added
theorem
Complex.hasStrictDerivAt_cosh
added
theorem
Complex.hasStrictDerivAt_sin
added
theorem
Complex.hasStrictDerivAt_sinh
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
DifferentiableWithinAt.ccos
added
theorem
DifferentiableWithinAt.ccosh
added
theorem
DifferentiableWithinAt.cos
added
theorem
DifferentiableWithinAt.cosh
added
theorem
DifferentiableWithinAt.csin
added
theorem
DifferentiableWithinAt.csinh
added
theorem
DifferentiableWithinAt.sin
added
theorem
DifferentiableWithinAt.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.ccosh
added
theorem
HasFDerivWithinAt.cos
added
theorem
HasFDerivWithinAt.cosh
added
theorem
HasFDerivWithinAt.csin
added
theorem
HasFDerivWithinAt.csinh
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.ccosh
added
theorem
HasStrictFDerivAt.cos
added
theorem
HasStrictFDerivAt.cosh
added
theorem
HasStrictFDerivAt.csin
added
theorem
HasStrictFDerivAt.csinh
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.differentiableAt_cos
added
theorem
Real.differentiableAt_cosh
added
theorem
Real.differentiableAt_sin
added
theorem
Real.differentiableAt_sinh
added
theorem
Real.differentiable_cos
added
theorem
Real.differentiable_cosh
added
theorem
Real.differentiable_sin
added
theorem
Real.differentiable_sinh
added
theorem
Real.hasDerivAt_cos
added
theorem
Real.hasDerivAt_cosh
added
theorem
Real.hasDerivAt_sin
added
theorem
Real.hasDerivAt_sinh
added
theorem
Real.hasStrictDerivAt_cos
added
theorem
Real.hasStrictDerivAt_cosh
added
theorem
Real.hasStrictDerivAt_sin
added
theorem
Real.hasStrictDerivAt_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
Real.sinh_sub_id_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