cosh_three_mul

Mathlib.Analysis.Complex.Trigonometric

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

English

For all x, cosh(3x) = 4 cosh^3 x - 3 cosh x.

Русский

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

LaTeX

$$$\\cosh(3x) = 4 \\cosh^3 x - 3 \\cosh x$$$

Lean4

nonrec theorem cosh_three_mul : cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x := by rw [← ofReal_inj];
  simp [cosh_three_mul]

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

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

Разделы

Аффилиация

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