sinh_three_mul

Mathlib.Analysis.Complex.Trigonometric

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

English

For all x, sinh(3x) = 4 sinh^3 x + 3 sinh x.

Русский

Для всех x: sinh(3x) = 4 sinh^3 x + 3 sinh x.

LaTeX

$$$\\sinh(3x) = 4 \\sinh^3 x + 3 \\sinh x$$$

Lean4

nonrec theorem sinh_three_mul : sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x := by rw [← ofReal_inj];
  simp [sinh_three_mul]

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

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

Разделы

Аффилиация

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