iteratedDeriv_add_one_cosh — Mathlib

English

The (n+1)-st derivative of cosh equals the nth derivative of sinh.

Русский

(n+1)-я производная от cosh равна n-й производной от sinh.

LaTeX

$$$\\\\frac{d^{n+1}}{dz^{n+1}} \\\\cosh z = \\\\frac{d^{n}}{dz^{n}} \\\\sinh z$$$

Lean4

@[simp]
theorem iteratedDeriv_add_one_cosh (n : ℕ) : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh := by
  induction n with
  | zero => ext; simp
  | succ n ih => rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

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