iteratedDeriv_even_cosh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Real.iteratedDeriv_even_cosh

← MathLib Explorer

English

The 2n-th derivative of cosh over the reals equals cosh.

Русский

2n-я производная от cosh на действительных равна cosh.

LaTeX

$$$\\\\frac{d^{2n}}{dx^{2n}} \\\\cosh x = (-1)^{0} \\\\cosh x$$$

Lean4

@[simp]
theorem iteratedDeriv_even_cosh (n : ℕ) : iteratedDeriv (2 * n) cosh = cosh := by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]

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

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

Разделы

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

Аффилиация

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