iteratedDeriv_add_one_sinh — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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