differentiable_iteratedDeriv_cosh

English

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

Русский

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

LaTeX

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

Lean4

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

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