cosh_three_mul — Mathlib

English

For all complex 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

theorem cosh_three_mul : cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x :=
  by
  have h1 : x + 2 * x = 3 * x := by ring
  rw [← h1, cosh_add x (2 * x)]
  simp only [cosh_two_mul, sinh_two_mul]
  have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2 := by ring
  rw [h2, sinh_sq]
  ring

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