iteratedDeriv_odd_cos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

English

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

Русский

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

LaTeX

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

Lean4

theorem iteratedDeriv_odd_cos (n : ℕ) : iteratedDeriv (2 * n + 1) cos = (-1) ^ (n + 1) * sin := by simp [pow_succ]

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

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

Разделы

Аффилиация

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