sinh_three_mul — Mathlib

English

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

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

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