cosh_mul_I

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Complex.cosh_mul_I

English

cosh(x I) = cos x.

Русский

cosh(x I) = cos x.

LaTeX

$$$\\cosh(x \\cdot \\mathrm{I}) = \\cos x$$$

Lean4

theorem cosh_mul_I : cosh (x * I) = cos x := by
  rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]

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

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

Разделы

Аффилиация

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