differentiable_iteratedDeriv_sinh

English

For every n, the n-th derivative of sinh, viewed as a function on the complex plane, is complex-differentiable.

Русский

Для каждого n-ого производного sinh, как функции на \u211d, выполняется комплексная дифференцируемость.

LaTeX

$$$\forall n \in \\mathbb{N},\\; z \\mapsto \\frac{d^{n}}{dz^{n}} \\sinh z \\text{ is entire on } \\mathbb{C}$$$

Lean4

theorem differentiable_iteratedDeriv_sinh (n : ℕ) : Differentiable ℂ (iteratedDeriv n sinh) :=
  match n with
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by simp [differentiable_iteratedDeriv_sinh]

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