Commit 2025-12-09 06:39 7221b013

View on Github →

refactor: split long file Analysis.SpecialFunctions.Trigonometric.Deriv (#32605) Results on hyperbolic trig functions moved to a different file.

Estimated changes

deleted theorem Complex.analyticAt_cosh
deleted theorem Complex.analyticAt_sinh
deleted theorem Complex.analyticOn_cosh
deleted theorem Complex.analyticOn_sinh
deleted theorem Complex.contDiff_cosh
deleted theorem Complex.contDiff_sinh
deleted theorem Complex.deriv_cosh
deleted theorem Complex.deriv_sinh
deleted theorem Complex.hasDerivAt_cosh
deleted theorem Complex.hasDerivAt_sinh
deleted theorem Complex.isEquivalent_sinh
deleted theorem Complex.logDeriv_cosh
deleted theorem ContDiff.ccosh
deleted theorem ContDiff.cosh
deleted theorem ContDiff.csinh
deleted theorem ContDiff.sinh
deleted theorem ContDiffAt.ccosh
deleted theorem ContDiffAt.cosh
deleted theorem ContDiffAt.csinh
deleted theorem ContDiffAt.sinh
deleted theorem ContDiffOn.ccosh
deleted theorem ContDiffOn.cosh
deleted theorem ContDiffOn.csinh
deleted theorem ContDiffOn.sinh
deleted theorem ContDiffWithinAt.ccosh
deleted theorem ContDiffWithinAt.cosh
deleted theorem ContDiffWithinAt.csinh
deleted theorem ContDiffWithinAt.sinh
deleted theorem Differentiable.ccosh
deleted theorem Differentiable.cosh
deleted theorem Differentiable.csinh
deleted theorem Differentiable.sinh
deleted theorem DifferentiableAt.ccosh
deleted theorem DifferentiableAt.cosh
deleted theorem DifferentiableAt.csinh
deleted theorem DifferentiableAt.sinh
deleted theorem DifferentiableOn.ccosh
deleted theorem DifferentiableOn.cosh
deleted theorem DifferentiableOn.csinh
deleted theorem DifferentiableOn.sinh
deleted theorem HasDerivAt.ccosh
deleted theorem HasDerivAt.cosh
deleted theorem HasDerivAt.csinh
deleted theorem HasDerivAt.sinh
deleted theorem HasDerivWithinAt.ccosh
deleted theorem HasDerivWithinAt.cosh
deleted theorem HasDerivWithinAt.csinh
deleted theorem HasDerivWithinAt.sinh
deleted theorem HasFDerivAt.ccosh
deleted theorem HasFDerivAt.cosh
deleted theorem HasFDerivAt.csinh
deleted theorem HasFDerivAt.sinh
deleted theorem HasFDerivWithinAt.ccosh
deleted theorem HasFDerivWithinAt.cosh
deleted theorem HasFDerivWithinAt.csinh
deleted theorem HasFDerivWithinAt.sinh
deleted theorem HasStrictDerivAt.ccosh
deleted theorem HasStrictDerivAt.cosh
deleted theorem HasStrictDerivAt.csinh
deleted theorem HasStrictDerivAt.sinh
deleted theorem HasStrictFDerivAt.ccosh
deleted theorem HasStrictFDerivAt.cosh
deleted theorem HasStrictFDerivAt.csinh
deleted theorem HasStrictFDerivAt.sinh
deleted theorem Real.abs_sinh
deleted theorem Real.analyticAt_cosh
deleted theorem Real.analyticAt_sinh
deleted theorem Real.analyticOnNhd_cosh
deleted theorem Real.analyticOnNhd_sinh
deleted theorem Real.analyticOn_cosh
deleted theorem Real.analyticOn_sinh
deleted theorem Real.contDiff_cosh
deleted theorem Real.contDiff_sinh
deleted theorem Real.cosh_le_cosh
deleted theorem Real.cosh_lt_cosh
deleted theorem Real.cosh_strictMonoOn
deleted theorem Real.deriv_cosh
deleted theorem Real.deriv_sinh
deleted theorem Real.differentiable_cosh
deleted theorem Real.differentiable_sinh
deleted theorem Real.hasDerivAt_cosh
deleted theorem Real.hasDerivAt_sinh
deleted theorem Real.isEquivalent_sinh
deleted theorem Real.logDeriv_cosh
deleted theorem Real.one_le_cosh
deleted theorem Real.one_lt_cosh
deleted theorem Real.self_le_sinh_iff
deleted theorem Real.self_lt_sinh_iff
deleted theorem Real.sinh_eq_zero
deleted theorem Real.sinh_inj
deleted theorem Real.sinh_injective
deleted theorem Real.sinh_le_self_iff
deleted theorem Real.sinh_le_sinh
deleted theorem Real.sinh_lt_self_iff
deleted theorem Real.sinh_lt_sinh
deleted theorem Real.sinh_ne_zero
deleted theorem Real.sinh_neg_iff
deleted theorem Real.sinh_nonneg_iff
deleted theorem Real.sinh_nonpos_iff
deleted theorem Real.sinh_pos_iff
deleted theorem Real.sinh_strictMono
deleted theorem derivWithin_ccosh
deleted theorem derivWithin_cosh
deleted theorem derivWithin_csinh
deleted theorem derivWithin_sinh
deleted theorem deriv_ccosh
deleted theorem deriv_cosh
deleted theorem deriv_csinh
deleted theorem deriv_sinh
deleted theorem fderivWithin_ccosh
deleted theorem fderivWithin_cosh
deleted theorem fderivWithin_csinh
deleted theorem fderivWithin_sinh
deleted theorem fderiv_ccosh
deleted theorem fderiv_cosh
deleted theorem fderiv_csinh
deleted theorem fderiv_sinh
added theorem Complex.contDiff_cosh
added theorem Complex.contDiff_sinh
added theorem Complex.deriv_cosh
added theorem Complex.deriv_sinh
added theorem Complex.logDeriv_cosh
added theorem ContDiff.ccosh
added theorem ContDiff.cosh
added theorem ContDiff.csinh
added theorem ContDiff.sinh
added theorem ContDiffAt.ccosh
added theorem ContDiffAt.cosh
added theorem ContDiffAt.csinh
added theorem ContDiffAt.sinh
added theorem ContDiffOn.ccosh
added theorem ContDiffOn.cosh
added theorem ContDiffOn.csinh
added theorem ContDiffOn.sinh
added theorem ContDiffWithinAt.ccosh
added theorem ContDiffWithinAt.cosh
added theorem ContDiffWithinAt.csinh
added theorem ContDiffWithinAt.sinh
added theorem Differentiable.ccosh
added theorem Differentiable.cosh
added theorem Differentiable.csinh
added theorem Differentiable.sinh
added theorem DifferentiableAt.ccosh
added theorem DifferentiableAt.cosh
added theorem DifferentiableAt.csinh
added theorem DifferentiableAt.sinh
added theorem DifferentiableOn.ccosh
added theorem DifferentiableOn.cosh
added theorem DifferentiableOn.csinh
added theorem DifferentiableOn.sinh
added theorem HasDerivAt.ccosh
added theorem HasDerivAt.cosh
added theorem HasDerivAt.csinh
added theorem HasDerivAt.sinh
added theorem HasDerivWithinAt.ccosh
added theorem HasDerivWithinAt.cosh
added theorem HasDerivWithinAt.csinh
added theorem HasDerivWithinAt.sinh
added theorem HasFDerivAt.ccosh
added theorem HasFDerivAt.cosh
added theorem HasFDerivAt.csinh
added theorem HasFDerivAt.sinh
added theorem HasFDerivWithinAt.cosh
added theorem HasFDerivWithinAt.sinh
added theorem HasStrictDerivAt.ccosh
added theorem HasStrictDerivAt.cosh
added theorem HasStrictDerivAt.csinh
added theorem HasStrictDerivAt.sinh
added theorem HasStrictFDerivAt.cosh
added theorem HasStrictFDerivAt.sinh
added theorem Real.abs_sinh
added theorem Real.analyticAt_cosh
added theorem Real.analyticAt_sinh
added theorem Real.analyticOn_cosh
added theorem Real.analyticOn_sinh
added theorem Real.contDiff_cosh
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_cosh
added theorem Real.deriv_sinh
added theorem Real.hasDerivAt_cosh
added theorem Real.hasDerivAt_sinh
added theorem Real.isEquivalent_sinh
added theorem Real.logDeriv_cosh
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_eq_zero
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_ne_zero
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_ccosh
added theorem derivWithin_cosh
added theorem derivWithin_csinh
added theorem derivWithin_sinh
added theorem deriv_ccosh
added theorem deriv_cosh
added theorem deriv_csinh
added theorem deriv_sinh
added theorem fderivWithin_ccosh
added theorem fderivWithin_cosh
added theorem fderivWithin_csinh
added theorem fderivWithin_sinh
added theorem fderiv_ccosh
added theorem fderiv_cosh
added theorem fderiv_csinh
added theorem fderiv_sinh