iteratedDeriv_add_one_cos — Mathlib

English

For all n ∈ ℕ, iteratedDeriv (n + 1) cos = - iteratedDeriv n sin.

Русский

Для любого n ∈ ℕ выполняется iteratedDeriv (n+1) cos = - iteratedDeriv n sin.

LaTeX

$$\forall n \in \mathbb{N}, \; \operatorname{iteratedDeriv} (n+1) \cos = -\operatorname{iteratedDeriv} n \sin$$

Lean4

@[simp]
theorem iteratedDeriv_add_one_cos (n : ℕ) : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin := by
  induction n with
  | zero => ext; simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']
    ext x
    simp

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