iteratedDeriv_even_cos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Complex.iteratedDeriv_even_cos

← MathLib Explorer

English

For all n ∈ ℕ, iteratedDeriv (2n) cos = (-1)^n cos.

Русский

Для каждого n ∈ ℕ верно: iteratedDeriv (2n) cos = (-1)^n cos.

LaTeX

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

Lean4

@[simp]
theorem iteratedDeriv_even_cos (n : ℕ) : iteratedDeriv (2 * n) cos = (-1) ^ n * cos := by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru