logDeriv_cosh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

← MathLib Explorer

English

For real numbers, logDeriv(Real.cosh) = Real.tanh.

Русский

Для вещественных чисел logDeriv(Real.cosh) = Real.tanh.

LaTeX

$$$\logDeriv(\mathrm{Real}.\cosh) = \mathrm{Real}.\tanh$$$

Lean4

@[simp]
theorem logDeriv_cosh : logDeriv (Real.cosh) = Real.tanh :=
  by
  ext
  rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]

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

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

Разделы

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

Аффилиация

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