iteratedDeriv_add_one_cosh — Mathlib

English

For all n ∈ ℕ, iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh.

Русский

Для каждого n ∈ ℕ выполняется iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh.

LaTeX

$$\forall n \in \mathbb{N}, \; \operatorname{iteratedDeriv} (n + 1) \cosh = \operatorname{iteratedDeriv} n \sinh$$

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]

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