fderiv_ccosh — Mathlib

English

If f is differentiable at x with derivative f', then the fderiv of cosh(f) at x equals sinh(f(x)) times f'(x).

Русский

Если f дифференцируема в x с производной f', то fderiv косh(f) в x равен sinh(f(x)) умноженному на f'(x).

LaTeX

$$$$ fderiv_{\mathbb{C}}(\cosh \circ f)(x) = \sinh(f(x)) \cdot fderiv_{\mathbb{C}} f(x). $$$$

Lean4

@[simp]
theorem fderiv_ccosh (hc : DifferentiableAt ℂ f x) :
    fderiv ℂ (fun x => Complex.cosh (f x)) x = Complex.sinh (f x) • fderiv ℂ f x :=
  hc.hasFDerivAt.ccosh.fderiv

Похожие утверждения